Definition catiso_inv_mor {y₁ y₂ : D} (f : y₁ --> y₂) : catiso_inv_ob y₁ --> catiso_inv_ob y₂ := fully_faithful_inv_hom catiso_to_fully_faithful _ _ (idtoiso (catiso_catiso_inv_ob y₁) · f · idtoiso (!(catiso_catiso_inv_ob y₂))).
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.