Lemma total_category_is_precat {C : category} (D : disp_cat C) : is_precategory (total_category_data D). 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.