Lemma coslice_cat_disp_id_comp : disp_cat_id_comp C coslice_cat_disp_ob_mor. Proof. split. - intros a f. apply id_right. - intros a1 a2 a3 h h' f1 f2 f3 Hyph Hyph'. etrans. { apply assoc. } etrans. { apply cancel_postcomposition, Hyph. } exact Hyph'. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.