Definition three_mor_eq' {C : category} {x y : three C} {f g : x --> y} (Hb: pr11 f = pr11 g) (H11: three_mor11 f = three_mor11 g) : f = g.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.