Definition doublecategory_to_twosided_disp_cat_data (C : doublecategory) : twosided_disp_cat_data (und_ob_hor_cat C) (und_ob_hor_cat C). Proof. use tpair. - use tpair. * intros x y. exact (x -v-> y). * intros x y z w f g h k. exact (sqq h f g k). - use tpair. * intros x y f. exact (hor_sq_identity f). * intros x y z a b c f1 f2 f3 f4 f5 f6 f7 α β. exact (α ·sqh β). Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.