proposition: 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: 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.
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