Lemma iso_from_fully_faithful_reflection_functor_on_iso (C : category)(D : precategory) (F : functor C D) (HF : fully_faithful F) (a b : ob C) (f : z_iso a b) : iso_from_fully_faithful_reflection HF (functor_on_z_iso F f) = f. Proof. apply z_iso_eq. simpl; apply (homotinvweqweq (weq_from_fully_faithful HF a b)). 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.