Proposition catiso_inv_mor_eq {y₁ y₂ : D} (f : y₁ --> y₂) (g : catiso_inv_ob y₁ --> catiso_inv_ob y₂) (p : f = idtoiso (!(catiso_catiso_inv_ob y₁)) · #F g · idtoiso (catiso_catiso_inv_ob y₂)) : catiso_inv_mor f = g. Proof. use (invmaponpathsweq (weq_from_fully_faithful catiso_to_fully_faithful _ _)). cbn -[catiso_inv_mor]. rewrite catiso_catiso_inv_mor. rewrite p. rewrite !assoc. etrans. { etrans. { do 3 apply maponpaths_2. refine (!_). apply pr1_idtoiso_concat. } rewrite pathsinv0r ; cbn. rewrite id_left. rewrite !assoc'. etrans. { apply maponpaths. refine (!_). apply (pr1_idtoiso_concat (catiso_catiso_inv_ob y₂)). } rewrite pathsinv0r ; cbn. apply id_right. } apply idpath. 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.