Declare iff as a transitive, symmetric reflexive relation. This chang…

…es the order of the arguments of iff_compose.

theories/Basics/Overture.v

@@ -147,13 +147,18 @@ Notation compose := (fun g f x => g (f x)).
 Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
 
 (** Composition of logical equivalences *)
-Definition iff_compose {A B C : Type} (g : B <-> C) (f : A <-> B)
-: A <-> C
-:= (fst g o fst f , snd f o snd g).
+Instance iff_compose : Transitive iff
+  := fun A B C f g => (fst g o fst f , snd f o snd g).
+Arguments iff_compose {A B C} f g : rename.
 
 (** While we're at it, inverses of logical equivalences *)
-Definition iff_inverse {A B : Type} : (A <-> B) -> (B <-> A)
-  := fun f => (snd f , fst f).
+Instance iff_inverse : Symmetric iff
+  := fun A B f => (snd f , fst f).
+Arguments iff_inverse {A B} f : rename.
+
+(** And reflexivity of them *)
+Instance iff_reflexive : Reflexive iff
+  := fun A => (idmap , idmap).
 
 (** Dependent composition of functions. *)
 Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x).

theories/Spaces/BAut/Cantor.v

@@ -145,8 +145,8 @@ Section Assumptions.
         (x : cantor + cantor + cantor + cantor)
   : (is_inr x + is_inl_and is_inr x) <-> is_inr (I0 x).
   Proof.
-    refine (iff_compose (f_flip_fixed_iff_inr (I0 x)) _).
-    refine (iff_compose (I0_fixed_iff_fixed x) _).
+    refine (iff_compose _ (f_flip_fixed_iff_inr (I0 x))).
+    refine (iff_compose _ (I0_fixed_iff_fixed x)).
     apply iff_inverse, ff_flip_fixed_iff_inr.
   Defined.