Proposition twosided_disp_cat_on_disp_cat_axioms : twosided_disp_cat_axioms twosided_disp_cat_on_disp_cat_data. Proof. repeat split. - intro ; intros. rewrite transportb_disp_mor2_twosided_disp_cat_on_disp_cat. refine (id_two_disp_left _ @ _). use transportb_disp_mor2_eq. apply idpath. - intro ; intros. rewrite transportb_disp_mor2_twosided_disp_cat_on_disp_cat. refine (id_two_disp_right _ @ _). use transportb_disp_mor2_eq. apply idpath. - intro ; intros. rewrite transportb_disp_mor2_twosided_disp_cat_on_disp_cat. refine (assoc_two_disp _ _ _ @ _). use transportb_disp_mor2_eq. apply idpath. - intro ; intros. apply isaset_disp_mor. Qed.
Require Import UniMath.Foundations.All. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total.