Definition id_is_gregarious_equivalence (x : B) : is_gregarious_equivalence (id_h x) (id_v x). Proof. repeat split. - apply id_are_companions. - apply internal_adjoint_equivalence_identity. - apply internal_adjoint_equivalence_identity. Defined.
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.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairs. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairAdjEquiv.