Lemma fully_faithful_inv_identity (C D : precategory_data) (F : functor C D) (FF : fully_faithful F) (a : ob C) : FF^-1 (identity (F a)) = identity _. Proof. apply (invmaponpathsweq (weq_from_fully_faithful FF a a)). unfold fully_faithful_inv_hom. set (HFaa:=homotweqinvweq (weq_from_fully_faithful FF a a)(identity _ )). simpl in *. rewrite HFaa. rewrite functor_id; apply idpath. 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.