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. intros. apply (nat_trans_eq (homset_property E)). intro x. unfold horcomp, horcomp_data. cbn. apply pathsinv0. apply nat_trans_ax. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.