proposition: Lemma interchange_functorial_composition (A B C: category) (F1 G1 H1: A ⟶ B) (F2 G2 H2: B ⟶ C) (α1 : F1 ⟹ G1) (α2: F2 ⟹ G2) (β1: G1 ⟹ H1) (β2: G2 ⟹ H2): # (functorial_composition A B C) (catbinprodmor ((α1:(functor_category A B)⟦F1,G1⟧) · β1) ((α2:(functor_category B C)⟦F2,G2⟧) · β2)) = # (functorial_composition A B C) (catbinprodmor(C:=functor_category A B)(D:=functor_category B C) α1 α2) · # (functorial_composition A B C) (catbinprodmor(C:=functor_category A B)(D:=functor_category B C) β1 β2).
proof: Proof. exact (hcomp_vcomp A B C F1 G1 H1 F2 G2 H2 α1 α2 β1 β2). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.Core.Bicat