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

--------------------------------------------------------------------------------
-- Lemma 5.8 for a general path interval.
--
-- From the path presentation of a (not necessarily fibrant) path interval we
-- derive the coercion operation and its laws (c1)–(c3), and hence discharge the
-- coercion interface of `WeakGlueUA`, giving Theorem 5.14 for a
-- general path interval.
--
-- We package clause (2) of Definition 5.6 as the interface it delivers
-- (`PathStructure`): for every fibrant `Y` (here at level `lsuc 𝓤`, large enough
-- for `UU 𝓤`, the function classifier `U→`, and constant families), a
-- line-to-identity operation on lines into `Y`, valued in the identity type of
-- the endpoints, and natural in `Y`.  Nothing else is assumed; in particular
-- degeneracy on constant lines is *derived* (`path-const` below), not required.
--
--   coe^G ≔ π₁(idtoeqv(path G)),
--   (c1) definitional;
--   (c2) naturality, via the function classifier `U→` and the path-in-`U→`
--        lemma `key` (path induction) + naturality of `path`;
--   (c3) degeneracy, from the derived `path-const`.
--
-- The derivation of `path-const` is the paper's derivation of
-- Lemma 5.8(c3): the constant line λ_. y factors as (λ_. y) ∘ !I
-- through the terminal line !I : I → ⊤, the path of !I lives in the
-- contractible Id ⋆ ⋆ and hence equals refl, and naturality transports this to
-- the constant family.
--------------------------------------------------------------------------------

module Extension.CoercionLaws where

open import Extension.Prelude
open import Extension.GlueRules using (WeakGlue)
open import Extension.WeakGlueUA using (weak-glue-implies-ua)

private
  variable
    ℓI 𝓤 : Level

record PathStructure (ℓI 𝓤 : Level) : UUᵉ (lsuc (ℓI ⊔ lsuc 𝓤)) where
  field
    I    : UUᵉ ℓI
    0I 1I : I
    path : {Y : UU (lsuc 𝓤)} (g : I → C Y) → Id (ic (g 0I)) (ic (g 1I))
    path-nat : {Y Z : UU (lsuc 𝓤)} (h : Y → Z) (g : I → C Y)
             → Id (ap h (path g)) (path (λ t → c (h (ic (g t)))))

module _ (P : PathStructure ℓI 𝓤) where
  open PathStructure P

  private
    -- the terminal line, and its path: it lives in Id ⋆ ⋆, which is a
    -- proposition, so it is refl
    !I : I → C (⊤ {lsuc 𝓤})
    !I _ = c star

    path-!-refl : Id (path !I) refl
    path-!-refl =
      is-set-to-all-paths-equal (⊤ {lsuc 𝓤})
        (is-set-is-contr (⊤ {lsuc 𝓤}) (star , (λ _ → refl)))
        star star (path !I) refl

  -- degeneracy on constant lines, derived from naturality at Y = ⊤
  path-const : {Y : UU (lsuc 𝓤)} (y : Y) → Id (path {Y} (λ _ → c y)) refl
  path-const {Y} y = (path-nat (λ _ → y) !I) ⁻¹ · ap (ap (λ _ → y)) path-!-refl

  private
    -- the function classifier  U→ = Σ(X,Y:𝓤). X → Y
    U→ : UU (lsuc 𝓤)
    U→ = Σ (UU 𝓤) (λ X → Σ (UU 𝓤) (λ Y → (X → Y)))
    dom : U→ → UU 𝓤
    dom w = pr1 w
    cod : U→ → UU 𝓤
    cod w = pr1 (pr2 w)
    fn : (w : U→) → dom w → cod w
    fn w = pr2 (pr2 w)

    path-univ : (G : I → UU 𝓤) → Id (G 0I) (G 1I)
    path-univ G = path {UU 𝓤} (λ t → c (G t))

    coe : (G : I → UU 𝓤) → G 0I → G 1I
    coe G = pr1 (idtoeqv (path-univ G))

    c1 : (G : I → UU 𝓤) (x : G 0I) → Id (coe G x) (pr1 (idtoeqv (path-univ G)) x)
    c1 G x = refl

    c3 : (Y : UU 𝓤) (x : Y) → Id (coe (λ _ → Y) x) x
    c3 Y x = ap (λ p → pr1 (idtoeqv p) x) (path-const {UU 𝓤} Y)

    -- path-in-U→ lemma: a path in U→ gives the naturality square (path induction)
    key : (ξ : I → C U→) (w : U→) (r : Id (ic (ξ 0I)) w) (x : dom (ic (ξ 0I)))
        → Id (pr1 (idtoeqv (ap cod r)) (fn (ic (ξ 0I)) x))
             (fn w (pr1 (idtoeqv (ap dom r)) x))
    key ξ w refl x = refl

    c2 : (G H : I → UU 𝓤) (θ : (t : I) → G t → H t) (x : G 0I)
       → Id (θ 1I (coe G x)) (coe H (θ 0I x))
    c2 G H θ x =
      (sub-cod ⁻¹ · (key ξ (ic (ξ 1I)) (path ξ) x · sub-dom)) ⁻¹
      where
      ξ : I → C U→
      ξ t = c (G t , (H t , θ t))
      sub-cod : Id (pr1 (idtoeqv (ap cod (path ξ))) (θ 0I x)) (coe H (θ 0I x))
      sub-cod = ap (λ p → pr1 (idtoeqv p) (θ 0I x)) (path-nat cod ξ)
      sub-dom : Id (θ 1I (pr1 (idtoeqv (ap dom (path ξ))) x)) (θ 1I (coe G x))
      sub-dom = ap (λ p → θ 1I (pr1 (idtoeqv p) x)) (path-nat dom ξ)

  -- Theorem 5.14 for a general path interval.
  general-weak-glue-implies-ua :
      WeakGlue I 0I 1I 𝓤 → (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})
  general-weak-glue-implies-ua =
    weak-glue-implies-ua I 0I 1I 𝓤 coe path-univ c1 c2 c3