proposition: Lemma functor_identity_right (C D : precategory) (F : functor C D) : functor_composite F (functor_identity D) = F.
proof: Proof. destruct F as [ [ Fob Fmor ] is ] . apply ( maponpaths ( λ p, tpair is_functor (tpair _ Fob Fmor) p ) ) . destruct is as [ idax compax ] . apply pathsdirprod . simpl . apply funextsec . intro t . unfold functor_identity . unfold functor_id . simpl . rewrite maponpathsidfun . rewrite pathscomp0rid . apply idpath . apply funextsec . intro t . apply funextsec . intro t0 . apply funextsec . intro t1 . apply funextsec . intro f . apply funextsec . intro g . unfold functor_identity . simpl . unfold functor_comp . simpl . rewrite maponpathsidfun . rewrite pathscomp0rid . apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence