proposition: Lemma total_category_is_precat {C : category} (D : disp_cat C) : is_precategory (total_category_data D).
proof: Proof. apply is_precategory_one_assoc_to_two. repeat apply tpair; simpl. - intros xx yy ff; cbn. use total2_paths_f; simpl. apply id_left. eapply pathscomp0. apply maponpaths, id_left_disp. apply transportfbinv. - intros xx yy ff; cbn. use total2_paths_f; simpl. apply id_right. eapply pathscomp0. apply maponpaths, id_right_disp. apply transportfbinv. - intros xx yy zz ww ff gg hh. use total2_paths_f; simpl. apply assoc. eapply pathscomp0. apply maponpaths, assoc_disp. apply transportfbinv. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence