proposition: Lemma is_precategory_coslice_precat_data : is_precategory coslice_precat_data.
proof: Proof. use make_is_precategory; intros; unfold comp_coslice_precat; cbn; apply subtypePairEquality. * intro; apply C. * apply id_left. * intro; apply C. * apply id_right. * intro; apply C. * apply assoc. * intro; apply C. * apply assoc'. Defined.
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