proposition: Proposition twosided_disp_cat_product_axioms : twosided_disp_cat_axioms twosided_disp_cat_product_data.
proof: 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.
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