Lemma functor_identity_right (C D : precategory) (F : functor C D) : functor_composite F (functor_identity D) = F. 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.
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.