Definition strict_underlying_vertical_two_cat_data : two_cat_data. Proof. use make_two_cat_data. - exact strict_underlying_vertical_precategory_data. - exact (λ x y v₁ v₂, s_square v₁ v₂ (s_identity_h x) (s_identity_h y)). - exact (λ x y v, s_id_h_square v). - exact (λ x y v₁ v₂ v₃ s₁ s₂, transportf_s_square (idpath _) (idpath _) (s_id_h_left _) (s_id_h_left _) (s₁ ⋆h s₂)). - exact (λ x y z v w₁ w₂ s, s_id_h_square v ⋆v s). - exact (λ x y z v₁ v₂ w s, s ⋆v s_id_h_square w). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.StrictDoubleCats.