[ setoid_rewrite (iso_comp1 i1) | setoid_rewrite (iso_comp2 i2) ];
reflexivity.
Defined.
+Notation "a >>≅>> b" := (iso_comp a b).
Definition functors_preserve_isos `{C1:Category}`{C2:Category}{Fo}(F:Functor C1 C2 Fo){a b:C1}(i:Isomorphic a b)
: Isomorphic (F a) (F b).
Reserved Notation "C 'ᵒᴾ'" (at level 1).
Reserved Notation "F \ a" (at level 20).
Reserved Notation "f >>> g" (at level 45).
+Reserved Notation "a >>≅>> b" (at level 45).
Reserved Notation "a ~~ b" (at level 54).
Reserved Notation "a ~> b" (at level 70, right associativity).
Reserved Notation "a ≃ b" (at level 70, right associativity).