Proposition idto2mor_right {a b : C} {f g g' : a --> b} (p p' : g = g') {τ τ' : 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.