proposition: Lemma coslice_cat_disp_id_comp : disp_cat_id_comp C coslice_cat_disp_ob_mor.
proof: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total