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.

Local Open Scope cat.
Local Open Scope double_bicat.

Section Univalence.
  Context (B : verity_double_bicat).

  Definition hor_globally_univalent
    : UU
    := is_univalent_2_0 (hor_bicat_of_verity_double_bicat B).

  Proposition isaprop_hor_globally_univalent
    : isaprop hor_globally_univalent.
  Proof.
    apply isaprop_is_univalent_2_0.
  Qed.

  Definition ver_globally_univalent
    : UU
    := is_univalent_2_0 (ver_bicat_of_verity_double_bicat B).

  Proposition isaprop_ver_globally_univalent
    : isaprop ver_globally_univalent.
  Proof.
    apply isaprop_is_univalent_2_0.
  Qed.

  Definition globally_univalent_verity_double_bicat
    : UU
    := hor_globally_univalent
       ×
       ver_globally_univalent.

  Proposition isaprop_globally_univalent_verity_double_bicat
    : isaprop globally_univalent_verity_double_bicat.
  Proof.
    apply isapropdirprod.
    - exact isaprop_hor_globally_univalent.
    - exact isaprop_ver_globally_univalent.
  Qed.

  Definition gregarious_univalent
    : UU
    := ∏ (x y : B), isweq (@id_to_gregarious_equivalence B x y).

  Proposition isaprop_gregarious_univalent
    : isaprop gregarious_univalent.
  Proof.
    do 2 (use impred ; intro).
    apply isapropisweq.
  Qed.

  Definition univalent_verity_double_bicat
    : UU
    := gregarious_univalent × locally_univalent_verity_double_bicat B.

  Proposition isaprop_univalent_verity_double_bicat
    : isaprop univalent_verity_double_bicat.
  Proof.
    use isapropdirprod.
    - exact isaprop_gregarious_univalent.
    - apply isaprop_locally_univalent_verity_double_bicat.
  Qed.

  Definition hor_globally_univalent_to_gregarious_univalent
             (HB_2_1 : locally_univalent_verity_double_bicat B)
             (HB_2_0 : hor_globally_univalent)
             (H : vertically_saturated B)
    : gregarious_univalent.
  Proof.
    intros x y.
    use weqhomot.
    - refine (weqfibtototal
                _ _
                (hor_left_adjoint_equivalence_weq_gregarious_equivalence _ _ H)
              ∘ make_weq _ (HB_2_0 x y))%weq.
      + apply HB_2_1.
      + use univalent_2_0_weakly_hor_invariant.
        apply HB_2_0.
    - intro p.
      induction p.
      use subtypePath.
      {
        intro.
        use (isofhlevelweqf
               1
               (is_hor_gregarious_equivalence_weq_is_gregarious_equivalence _)).
        apply (isaprop_is_hor_gregarious_equivalence H) ; apply HB_2_1.
      }
      apply idpath.
  Qed.

  Definition gregarious_univalent_to_hor_globally_univalent
             (H' : weakly_hor_invariant B)
             (HB_2_1 : locally_univalent_verity_double_bicat B)
             (HB_2_0 : gregarious_univalent)
             (H : vertically_saturated B)
    : hor_globally_univalent.
  Proof.
    intros x y.
    use weqhomot.
    - refine (weqfibtototal
               _ _
               (λ h, invweq
                       (hor_left_adjoint_equivalence_weq_gregarious_equivalence
                          _ _ H h))
             ∘ make_weq _ (HB_2_0 x y))%weq.
      + apply HB_2_1.
      + apply H'.
    - intro p.
      induction p.
      use subtypePath.
      {
        intro.
        apply isaprop_left_adjoint_equivalence.
        apply HB_2_1.
      }
      apply idpath.
  Qed.

  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.
End Univalence.