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

--------------------------------------------------------------------------------
-- Lemma 5.8 as named top-level statements.
--
--   coe               coe^G = π₁(idtoeqv(path G))
--   coercion-law-c1   (c1)  coe^G is the underlying map of idtoeqv(path G)
--   coercion-law-c2   (c2)  naturality:  θ₁ ∘ coe^G ∼ coe^H ∘ θ₀
--   coercion-law-c3   (c3)  degeneracy:  coe^{λ_.Y} ∼ id_Y
--
-- Extension.CoercionLaws derives all of these from a `PathStructure` but keeps
-- them private, exporting only the composite; the definitions are repeated
-- here term for term.  (c2) again goes through the function classifier
-- U→ = Σ(X,Y:𝓤).(X→Y) and the path-induction lemma `key`, combined with
-- naturality of the path presentation at dom and cod.
--------------------------------------------------------------------------------

module Extension.CoercionLawsNamed where

open import Extension.Prelude
open import Extension.CoercionLaws using (PathStructure ; path-const)

private
  variable
    ℓI 𝓤 : Level

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

  -- The universe-level path presentation of a line of types.
  path-univ : (G : I → UU 𝓤) → Id (G 0I) (G 1I)
  path-univ G = path {UU 𝓤} (λ t → c (G t))

  -- Lemma 5.8, the operation:  coe^G ≔ π₁(idtoeqv(path G)).
  coe : (G : I → UU 𝓤) → G 0I → G 1I
  coe G = pr1 (idtoeqv (path-univ G))

  -- (c1): coe^G is the underlying function of idtoeqv(path G), by definition.
  coercion-law-c1 : (G : I → UU 𝓤) (x : G 0I)
                  → Id (coe G x) (pr1 (idtoeqv (path-univ G)) x)
  coercion-law-c1 G x = 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-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) naturality: for a fibrewise map θ, one has θ₁ ∘ coe^G ∼ coe^H ∘ θ₀.
  coercion-law-c2 : (G H : I → UU 𝓤) (θ : (t : I) → G t → H t) (x : G 0I)
                  → Id (θ 1I (coe G x)) (coe H (θ 0I x))
  coercion-law-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 ξ)

  -- (c3) degeneracy: coercion in a constant family is (homotopic to) the
  -- identity.
  coercion-law-c3 : (Y : UU 𝓤) (x : Y) → Id (coe (λ _ → Y) x) x
  coercion-law-c3 Y x = ap (λ p → pr1 (idtoeqv p) x) (path-const P {UU 𝓤} Y)

  record CoercionPackage : UUᵉ (ℓI ⊔ lsuc 𝓤) where
    field
      coeP : (G : I → UU 𝓤) → G 0I → G 1I
      c1 : (G : I → UU 𝓤) (x : G 0I)
        → Id (coeP G x) (pr1 (idtoeqv (path-univ G)) x)
      c2 : (G H : I → UU 𝓤)
        (θ : (t : I) → G t → H t) (x : G 0I)
        → Id (θ 1I (coeP G x)) (coeP H (θ 0I x))
      c3 : (Y : UU 𝓤) (x : Y)
        → Id (coeP (λ _ → Y) x) x

  coercion-package : CoercionPackage
  coercion-package = record
    { coeP = coe
    ; c1 = coercion-law-c1
    ; c2 = coercion-law-c2
    ; c3 = coercion-law-c3
    }