Definition square_ver_sq_bicat_ver_id_comp : ver_sq_bicat_ver_id_comp square_ver_sq_bicat. Proof. split. - split. + exact (λ x, id₁ x). + exact (λ _ _ _ f g, f · g). - exact (λ x y v₁ v₂, v₂ ==> v₁). 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.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.