proposition: Lemma coslice_cat_disp_locally_prop : locally_propositional coslice_cat_disp_data.
proof: Proof. intro; intros; apply C. 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