Definition doublecategory_to_twosided_disp_cat (C : doublecategory) : twosided_disp_cat (und_ob_hor_cat C) (und_ob_hor_cat C). Proof. use tpair. - exact (doublecategory_to_twosided_disp_cat_data C). - repeat split. + intros x0 x1 y0 y1 f0 f1 g0 g1 α. exact (id_hor_sq_left α). + intros x0 x1 y0 y1 f0 f1 g0 g1 α. exact (id_hor_sq_right α). + intros ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? α β γ. exact (assoc_sq_hor α β γ). + intros x0 x1 y0 y1 f0 g0 f1 g1. exact (get_has_sq_hor_homsets f0 g0 f1 g1). 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.