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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.