Lemma is_univalent_total_category {C : category} {D : disp_cat C} (CC : is_univalent C) (DD : is_univalent_disp D) : is_univalent (total_category D). Proof. intros xs ys. set (x := pr1 xs). set (xx := pr2 xs). set (y := pr1 ys). set (yy := pr2 ys). use weqhomot. apply (@weqcomp _ (∑ e : x = y, transportf _ e xx = yy) _). apply total2_paths_equiv. apply (@weqcomp _ (∑ e : x = y, z_iso_disp (idtoiso e) xx yy) _). apply weqfibtototal. intros e. exists (λ ee, idtoiso_disp e ee). apply DD. apply (@weqcomp _ (∑ f : z_iso x y, z_iso_disp f xx yy) _). use (weqfp (make_weq _ _)). apply CC. apply total_z_iso_equiv. intros e; destruct e; apply z_iso_eq; cbn. apply idpath. 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.