proposition: Proposition isaprop_weakly_hor_invariant (B : verity_double_bicat) (H : vertically_saturated B) (HB_2_1 : locally_univalent_verity_double_bicat B) : isaprop (weakly_hor_invariant B).
proof: Proof. use impred ; intro x. use impred ; intro y. use impred ; intro h. use impred ; intro Hh. apply isaprop_companion_pair. - exact H. - exact HB_2_1. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairs