Lemma ff_reflects_is_iso (C D : precategory) (F : functor C D) (HF : fully_faithful F) : reflects_isos F. Proof. intros a b f H. set (X:= fully_faithful_reflects_iso_proof _ _ F HF _ _ (_,,H)). simpl in X. set (T:= homotinvweqweq (weq_from_fully_faithful HF a b ) ). simpl in T. unfold fully_faithful_inv_hom in X. simpl in X. rewrite T in X. apply X. 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.