Definition hor_globally_univalent_weq_gregarious_univalent (H' : weakly_hor_invariant B) (HB_2_1 : locally_univalent_verity_double_bicat B) (H : vertically_saturated B) : hor_globally_univalent ≃ gregarious_univalent. Proof. use weqimplimpl. - exact (λ HB_2_0, hor_globally_univalent_to_gregarious_univalent HB_2_1 HB_2_0 H). - exact (λ HB_2_0, gregarious_univalent_to_hor_globally_univalent H' HB_2_1 HB_2_0 H). - exact isaprop_hor_globally_univalent. - exact isaprop_gregarious_univalent. 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.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. 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. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.GregariousEquivalence.