Proposition twosided_disp_cat_product_axioms : twosided_disp_cat_axioms twosided_disp_cat_product_data. Proof. repeat split. - intro ; intros. rewrite transportb_twosided_disp_cat_product. use pathsdirprod. + refine (id_two_disp_left _ @ _). apply transportb_disp_mor2_eq. apply idpath. + refine (id_two_disp_left _ @ _). apply transportb_disp_mor2_eq. apply idpath. - intro ; intros. rewrite transportb_twosided_disp_cat_product. use pathsdirprod. + refine (id_two_disp_right _ @ _). apply transportb_disp_mor2_eq. apply idpath. + refine (id_two_disp_right _ @ _). apply transportb_disp_mor2_eq. apply idpath. - intro ; intros. rewrite transportb_twosided_disp_cat_product. use pathsdirprod. + refine (assoc_two_disp _ _ _ @ _). apply transportb_disp_mor2_eq. apply idpath. + refine (assoc_two_disp _ _ _ @ _). apply transportb_disp_mor2_eq. apply idpath. - intro ; intros. apply isaset_dirprod. + apply isaset_disp_mor. + apply isaset_disp_mor. Qed.
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.