proposition: Proposition catiso_inv_hom_idtoiso {x y : C} (p : F x = F y) : fully_faithful_inv_hom catiso_to_fully_faithful x y (idtoiso p) = idtoiso (catiso_reflect_ob_eq p).
proof: Proof. refine (!_ @ fully_faithful_inv_hom_is_inv catiso_to_fully_faithful _). apply maponpaths. refine (!(pr1_maponpaths_idtoiso F (catiso_reflect_ob_eq p)) @ _). apply setcategory_eq_idtoiso. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful