proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Equivalences.Core