Lemma is_precategory_coslice_precat_data : is_precategory coslice_precat_data. 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.
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.