Lemma functor_is_inverse_in_precat_inv_from_iso {C D : precategory} {c c' : ob C} (F : functor C D) (f : iso c c') : is_inverse_in_precat (# F f) (# F (inv_from_iso f)). Proof. apply functor_on_is_inverse_in_precat. split. + apply is_inverse_in_precat1. split. * apply (iso_inv_after_iso f). * apply (iso_after_iso_inv f). + apply is_inverse_in_precat2. split. * apply (iso_inv_after_iso f). * apply (iso_after_iso_inv f). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.