proposition: Lemma horcomp_post_pre (C D : category) (E : category) (F F' : functor C D) (G G' : functor D E) (f:nat_trans F F') (g:nat_trans G G') : horcomp f g = compose (C:=functor_category C E) (a:= (F ∙ G)) (b:= (F' ∙ G)) (c:= (F' ∙ G')) (post_whisker f G) (pre_whisker F' g).
proof: Proof. intros. apply (nat_trans_eq (homset_property E)). intro x. unfold horcomp, horcomp_data. cbn. apply pathsinv0. apply nat_trans_ax. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors