proposition: 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: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence