Definition is_univalent_constant_twosided_disp_cat (HD : is_univalent D) : is_univalent_twosided_disp_cat constant_twosided_disp_cat. Proof. intros x₁ x₂ y₁ y₂ p₁ p₂ z₁ z₂. induction p₁, p₂. use weqhomot. - exact (z_iso_weq_twosided_disp_cat_iso x₁ y₁ z₁ z₂ ∘ make_weq _ (HD z₁ z₂))%weq. - abstract (intro p ; cbn in p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; cbn ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.