Definition is_hor_gregarious_equivalence_weq_is_gregarious_equivalence {x y : B} (h : x --> y) : is_hor_gregarious_equivalence h ≃ (∑ (v : x -|-> y), is_gregarious_equivalence h v). Proof. use weq_iso. - exact (λ v, pr112 v ,, pr212 v ,, pr1 v ,, pr22 v). - intros v. use make_is_hor_gregarious_equivalence. + exact (pr1 v). + apply (pr2 v). + apply (pr2 v). + apply (pr2 v). - abstract (intro ; cbn ; apply idpath). - abstract (intro ; cbn ; apply idpath). 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.