Definition univalent_twosided_disp_cat_weq_univalent_disp_cat (C₁ C₂ : category) : univalent_twosided_disp_cat C₁ C₂ ≃ disp_univalent_category (category_binproduct C₁ C₂). Proof. use weqtotal2. - exact (two_sided_disp_cat_weq_disp_cat C₁ C₂). - exact (λ D, is_univalent_twosided_disp_cat_weq_is_univalent_disp_cat D). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.