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. exact (hcomp_vcomp A B C F1 G1 H1 F2 G2 H2 α1 α2 β1 β2). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.