Definition is_univalent_prod_of_twosided_disp_cat (HD₁ : is_univalent_twosided_disp_cat D₁) (HD₂ : is_univalent_twosided_disp_cat D₂) : is_univalent_twosided_disp_cat prod_of_twosided_disp_cat. Proof. intros x₁ x₂ y₁ y₂ p₁ p₂ xy₁ xy₂. induction p₁, p₂ ; cbn. use weqhomot. - exact (weq_iso_prod_of_twosided_disp_cat _ _ _ _ ∘ weqdirprodf (_ ,, HD₁ x₁ x₁ y₁ y₁ (idpath _) (idpath _) _ _) (_ ,, HD₂ x₁ x₁ y₁ y₁ (idpath _) (idpath _) _ _) ∘ pathsdirprodweq)%weq. - abstract (intro p ; induction p ; cbn ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; 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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.