Lemma fully_faithful_reflects_iso_proof (C D : precategory)(F : functor C D) (FF : fully_faithful F) (a b : ob C) (f : z_iso (F a) (F b)) : is_z_isomorphism (FF^-1 f). Proof. exists (FF^-1 (inv_from_z_iso f)). apply inv_of_ff_inv_is_inv. Defined.
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.