Lemma functor_assoc (C0 C1 C2 C3 : precategory) (F0 : functor C0 C1) (F1 : functor C1 C2) (F2 : functor C2 C3) : functor_composite (functor_composite F0 F1) F2 = functor_composite F0 (functor_composite F1 F2). Proof. destruct F0 as [ [ F0ob F0mor ] is0 ] . destruct F1 as [ [ F1ob F1mor ] is1 ] . destruct F2 as [ [ F2ob F2mor ] is2 ] . simpl . unfold functor_composite . simpl . apply ( maponpaths ( λ p, tpair is_functor _ p ) ) . simpl . apply pathsdirprod . apply funextsec . intro t . simpl . unfold functor_comp . simpl . unfold functor_id . simpl . unfold functor_id . simpl . destruct is0 as [ is0id is0comp ] . destruct is1 as [ is1id is1comp ] . destruct is2 as [ is2id is2comp ] . simpl . rewrite path_assoc. apply ( maponpaths ( λ e, pathscomp0 e ( is2id (F1ob (F0ob t)) ) ) ) . rewrite maponpathscomp0 . apply ( maponpaths ( λ e, pathscomp0 e ( maponpaths (F2mor (F1ob (F0ob t)) (F1ob (F0ob t))) (is1id (F0ob t)) ) ) ) . apply maponpathscomp . apply funextsec . intro t . apply funextsec . intro t0 . apply funextsec . intro t1 . apply funextsec . intro f . apply funextsec . intro g . simpl . unfold functor_comp . simpl . unfold functor_comp . simpl . destruct is0 as [ is0id is0comp ] . destruct is1 as [ is1id is1comp ] . destruct is2 as [ is2id is2comp ] . simpl . rewrite path_assoc. apply ( maponpaths ( λ e, pathscomp0 e ( is2comp (F1ob (F0ob t)) (F1ob (F0ob t0)) (F1ob (F0ob t1)) (F1mor (F0ob t) (F0ob t0) (F0mor t t0 f)) (F1mor (F0ob t0) (F0ob t1) (F0mor t0 t1 g)) ) ) ) . rewrite maponpathscomp0 . apply ( maponpaths ( λ e, pathscomp0 e ( maponpaths (F2mor (F1ob (F0ob t)) (F1ob (F0ob t1))) (is1comp (F0ob t) (F0ob t0) (F0ob t1) (F0mor t t0 f) (F0mor t0 t1 g)) ))). apply maponpathscomp . 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.