Definition double_cat_to_ver_sq_bicat_id_comp_cells : ver_sq_bicat_id_comp_cells double_cat_to_ver_sq_bicat_ver_id_comp. Proof. repeat split. - exact (λ (x y : ℍ) (f : x --> y), id2 f). - exact (λ (x y : ℍ) (f : x --> y), lunitor f). - exact (λ (x y : ℍ) (f : x --> y), runitor f). - exact (λ (x y : ℍ) (f : x --> y), linvunitor f). - exact (λ (x y : ℍ) (f : x --> y), rinvunitor f). - exact (λ (w x y z : ℍ) (f : w --> x) (g : x --> y) (h : y --> z), rassociator f g h). - exact (λ (w x y z : ℍ) (f : w --> x) (g : x --> y) (h : y --> z), lassociator f g h). - exact (λ (x y : ℍ) (f g h : x --> y) (τ : f ==> g) (θ : g ==> h), τ • θ). - exact (λ (x y z : ℍ) (f : x --> y) (g₁ g₂ : y --> z) (τ : g₁ ==> g₂), f ◃ τ). - exact (λ (x y z : ℍ) (f₁ f₂ : x --> y) (g : y --> z) (τ : f₁ ==> f₂), τ ▹ g). 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.Examples.DiscreteBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints. Require Import UniMath.Bicategories.DoubleCategories.Underlying.HorizontalBicategory.