Proposition idto2mor_left {a b : C} {f f' g : a --> b} (p p' : f = f') {τ τ' : f' ==> g} (r : τ = τ') : idto2mor p • τ = idto2mor p' • τ'. Proof. assert (p = p') as s. { apply homset_property. } induction s. induction r. apply idpath. Qed.
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.