Proposition is_univalent_twosided_disp_cat_product (HD₁ : is_univalent_twosided_disp_cat D₁) (HD₂ : is_univalent_twosided_disp_cat D₂) : is_univalent_twosided_disp_cat twosided_disp_cat_product. Proof. intros wx₁ wx₂ yz₁ yz₂ p q d₁ d₂. induction p, q. use weqhomot. - exact (twosided_disp_cat_product_iso_weq d₁ d₂ ∘ weqdirprodf (make_weq _ (HD₁ _ _ _ _ (idpath (pr1 wx₁)) (idpath (pr1 yz₁)) (pr1 d₁) (pr1 d₂))) (make_weq _ (HD₂ _ _ _ _ (idpath (pr2 wx₁)) (idpath (pr2 yz₁)) (pr2 d₁) (pr2 d₂))) ∘ pathsdirprodweq)%weq. - abstract (intro p ; cbn in p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; apply idpath). Defined.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.