Definition three_disp_ob_mor : disp_cat_ob_mor (arrow C). Proof. use make_disp_cat_ob_mor. - exact ((λ xy, ∑ z (xz : (arrow_dom xy) --> z) (zy : z --> (arrow_cod xy)), xz · zy = arrow_mor xy)). - intros xy ab H0 H1 fff. set (z := pr1 H0). set (xz := pr12 H0). set (zy := pr122 H0). set (c := pr1 H1). set (ac := pr12 H1). set (cb := pr122 H1). set (f0 := pr11 fff). set (f1 := pr21 fff). exact (∑ (f : z --> c), (xz · f = f0 · ac) × (zy · f1 = f · cb)). Defined.
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.