Definition horizontal_dual_twosided_disp_cat_data : twosided_disp_cat_data horizontal_dual_hor_bicat horizontal_dual_hor_bicat. Proof. simple refine ((_ ,, _) ,, (_ ,, _)). - exact (λ (x y : B), x -|-> y). - exact (λ (x₁ x₂ y₁ y₂ : B) (v₁ : x₁ -|-> y₁) (v₂ : x₂ -|-> y₂) (h₁ : x₂ --> x₁) (h₂ : y₂ --> y₁), square_double_bicat h₁ h₂ v₂ v₁). - exact (λ (x y : B) (v : x -|-> y), id_h_square_bicat _). - exact (λ (x₁ x₂ x₃ y₁ y₂ y₃ : B) (v₁ : x₁ -|-> y₁) (v₂ : x₂ -|-> y₂) (v₃ : x₃ -|-> y₃) (h₁ : x₂ --> x₁) (h₂ : x₃ --> x₂) (k₁ : y₂ --> y₁) (k₂ : y₃ --> y₂) (s₁ : square_double_bicat h₁ k₁ v₂ v₁) (s₂ : square_double_bicat h₂ k₂ v₃ v₂), s₂ ⋆h s₁). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence.