proposition: Lemma Functor_preserves_iso : forall (F : Functor C D) (a b : C), Iso a b -> Iso (F a) (F b).
proof: Proof. intros F a b f. apply Build_Iso with (FMor F (Iso_mor f)) (FMor F (Inv_iso f)). red in |- *; split; red in |- *. apply Trans with (FMor F (Inv_iso f o Iso_mor f)). apply FComp1. apply Trans with (FMor F (Id b)). apply FPres; apply (Idl_inv f). apply FId. apply Trans with (FMor F (Iso_mor f o Inv_iso f)). apply FComp1. apply Trans with (FMor F (Id a)). apply FPres; apply (Idr_inv f). apply FId. Qed.
imports: Functor CatProperty