Definition three_id_comp : disp_cat_id_comp _ three_disp_ob_mor. Proof. split. - intros. exists (identity _). abstract (split; now rewrite id_left, id_right). - intros x y z f g xx yy zz X Y. set (f0 := pr1 X). set (H0 := pr12 X). set (H1 := pr22 X). set (g0 := pr1 Y). set (K0 := pr12 Y). set (K1 := pr22 Y). exists (f0 · g0). abstract ( split; [ etrans; [apply assoc|]; etrans; [apply cancel_postcomposition, H0|]; etrans; [apply assoc'|]; etrans; [apply maponpaths; exact K0|]; apply assoc | apply pathsinv0; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition, (pathsinv0 K1)|]; etrans; [apply assoc|]; apply pathsinv0; etrans; [apply assoc|]; apply cancel_postcomposition; exact H1 ] ). 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.