Definition rwhisker_comp_mor {a b c d : C} {f g : a --> b} (τ : f ==> g) (h : b --> c) (i : c --> d) : τ ▹ h · i = two_cat_lassociator _ _ _ • (τ ▹ h ▹ i) • two_cat_rassociator _ _ _.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Univalence.