Proposition catiso_inv_mor_cat_iso {x₁ x₂ : C} (f : x₁ --> x₂) : catiso_inv_mor (#F f) = idtoiso (catiso_inv_ob_catiso x₁) · f · idtoiso (!(catiso_inv_ob_catiso x₂)). Proof. unfold catiso_inv_mor. rewrite !fully_faithful_inv_comp. rewrite fully_faithful_inv_hom_is_inv. rewrite !catiso_inv_hom_idtoiso. apply setcategory_eq_idtoiso_comp. 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.