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