Definition compose2h {C : prebicategory_id_comp} {a b c : C} {f f' : a -1-> b} {g g' : b -1-> c} (alpha : f -2-> f') (beta : g -2-> g') : (f ;1; g) -2-> (f' ;1; g'). Proof. apply functor_on_morphisms. exact (catbinprodmor alpha beta). Defined.
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.