Definition doublecategory_to_horcomp : hor_comp D. Proof. use make_hor_comp. - use make_hor_comp_data. + intros x y z f g. exact (ver_compose f g). + cbn in *. intros x1 x2 y1 y2 z1 z2 v1 v2 v3 h1 h2 k1 k2 α β. exact (ver_sq_compose α β). - split. + cbn in *. intros x y z f g. exact (get_predoublecategory_interchange_id_ver f g). + cbn in *. intros a0 a1 a2 b0 b1 b2 c0 c1 c2 fa ga fb gb fc gc h0 k0 h1 k1 h2 k2 α β γ δ. exact (get_predoublecategory_interchange_comp α β γ δ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.AlternativeDefinitions.DoubleCatsUnfolded.