Lemma interchange {C : prebicategory} {a b c : C} {f1 f2 f3 : a -1-> b} {g1 g2 g3 : b -1-> c} (a1 : f1 -2-> f2) (a2 : f2 -2-> f3) (b1 : g1 -2-> g2) (b2 : g2 -2-> g3) : (a1 ;v; a2) ;h; (b1 ;v; b2) = (a1 ;h; b1) ;v; (a2 ;h; b2). Proof. unfold compose2h. assert (X : catbinprodmor a1 b1 · catbinprodmor a2 b2 = catbinprodmor (a1 ;v; a2) (b1 ;v; b2)) by reflexivity. rewrite <- X. apply functor_comp. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Equivalences.Core.