Definition arr_idto2mor_eq {a b : C} {f f' g g' : a --> b} (p p' : f = f') {τ τ' : f' ==> g} (q q' : g = g') (r : τ = τ') : idto2mor p • τ • idto2mor q = idto2mor p' • τ' • idto2mor q'.
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.