proposition: 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: 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.
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