{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- Theorem 5.14: a weak Glue structure for (I,0,1,𝓤), together with the coercion operation and
-- its laws (c1)–(c3) of Lemma 5.8, implies that 𝓤 is univalent.
--
-- Following the paper: given f : A ≃ B and the weak-glue data (G, b₀, b₁, u,
-- homotopies), set
--     s(f) ≔ b₀⁻¹ · path(G) · b₁ : A =_𝓤 B .
-- Using the groupoid action of idtoeqv and the coercion laws, the underlying map
-- of idtoeqv(s(f)) is
--     idtoeqv(b₁) ∘ coe^G ∘ idtoeqv(b₀)⁻¹
-- and the weak-glue homotopies (4) with naturality (c2) and degeneracy (c3)
-- collapse it to f.  Hence idtoeqv(s(f)) ~ f, so (isEquiv being a proposition)
-- idtoeqv(s(f)) = f; thus s is a section of idtoeqv, and `ua-from-section`
-- (Lemma 5.10) yields univalence.
--
-- The coercion operation `coe` and laws (c1) through (c3) form this module's
-- interface. `Extension.CoercionLaws` derives that interface from a path
-- interval.
--------------------------------------------------------------------------------

module Extension.WeakGlueUA where

open import Extension.Prelude
open import Extension.GlueRules using (WeakGlue)
open import Extension.UAFromSection using (ua-from-section)

private
  variable
    ℓI : Level

module _ (I : UUᵉ ℓI) (0I 1I : I) (𝓤 : Level)
         (coe       : (G : I → UU 𝓤) → G 0I → G 1I)
         (path-univ : (G : I → UU 𝓤) → Id (G 0I) (G 1I))
         (c1 : (G : I → UU 𝓤) (x : G 0I) → Id (coe G x) (pr1 (idtoeqv (path-univ G)) x))
         (c2 : (G H : I → UU 𝓤) (θ : (t : I) → G t → H t) (x : G 0I)
             → Id (θ 1I (coe G x)) (coe H (θ 0I x)))
         (c3 : (Y : UU 𝓤) (x : Y) → Id (coe (λ _ → Y) x) x)
       where

  private
    -- groupoid action of idtoeqv on a concatenation (path induction)
    idtoeqv-· : {X Y Z : UU 𝓤} (p : Id X Y) (q : Id Y Z) (x : X)
              → Id (pr1 (idtoeqv (p · q)) x) (pr1 (idtoeqv q) (pr1 (idtoeqv p) x))
    idtoeqv-· refl q x = refl

    -- idtoeqv of a path cancels idtoeqv of its inverse (path induction)
    idtoeqv-inv-sec : {X Y : UU 𝓤} (p : Id X Y) (x : Y)
                    → Id (pr1 (idtoeqv p) (pr1 (idtoeqv (p ⁻¹)) x)) x
    idtoeqv-inv-sec refl x = refl

  weak-glue-implies-ua : WeakGlue I 0I 1I 𝓤
                       → (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})
  weak-glue-implies-ua wg = ua-from-section secmap sect
    where
    secmap : (A B : UU 𝓤) → (A ≃ B) → Id A B
    secmap A B g = ((ic b₀) ⁻¹) · (path-univ G · ic b₁)
      where
      w  = wg A B (c g)
      G  = pr1ᵉ w
      b₀ = pr1ᵉ (pr2ᵉ w)
      b₁ = pr1ᵉ (pr2ᵉ (pr2ᵉ w))

    sect : (A B : UU 𝓤) (g : A ≃ B) → Id (idtoeqv (secmap A B g)) g
    sect A B g = dep-pair⁼ _ _ (funext ptwise , pr1 (is-prop-isEquiv (pr1 g) _ _))
      where
      w  = wg A B (c g)
      G  = pr1ᵉ w
      b₀ = pr1ᵉ (pr2ᵉ w)
      b₁ = pr1ᵉ (pr2ᵉ (pr2ᵉ w))
      u  = pr1ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ w)))
      H₀ = ic (pr1ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ w)))))
      H₁ = ic (pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ w)))))
      β₀ = ic b₀
      β₁ = ic b₁
      P  = path-univ G
      uf : (t : I) → G t → B
      uf t = ic (u t)

      ptwise : (x : A) → Id (pr1 (idtoeqv (secmap A B g)) x) (pr1 g x)
      ptwise x = chain0 · (step1 · (step2 · (step3 · (step4 · step5))))
        where
        y : G 0I
        y = pr1 (idtoeqv (β₀ ⁻¹)) x
        chain0 : Id (pr1 (idtoeqv (secmap A B g)) x) (pr1 (idtoeqv β₁) (coe G y))
        chain0 = idtoeqv-· (β₀ ⁻¹) (P · β₁) x
               · (idtoeqv-· P β₁ y
                 · ap (pr1 (idtoeqv β₁)) ((c1 G y) ⁻¹))
        step1 : Id (pr1 (idtoeqv β₁) (coe G y)) (uf 1I (coe G y))
        step1 = (H₁ (coe G y)) ⁻¹
        step2 : Id (uf 1I (coe G y)) (coe (λ _ → B) (uf 0I y))
        step2 = c2 G (λ _ → B) uf y
        step3 : Id (coe (λ _ → B) (uf 0I y)) (uf 0I y)
        step3 = c3 B (uf 0I y)
        step4 : Id (uf 0I y) (pr1 g (pr1 (idtoeqv β₀) y))
        step4 = H₀ y
        step5 : Id (pr1 g (pr1 (idtoeqv β₀) y)) (pr1 g x)
        step5 = ap (pr1 g) (idtoeqv-inv-sec β₀ x)