cubical-transport-hott-lean4/CubicalTransport/Typing.lean

/-
  CubicalTransport.Typing
  ======================
  The typing judgment  Γ ⊢ t : A  for the cubical term language,
  universe-stratified (Layer 0 §0.1 cascade).

  Rules:
    var   : membership in context
    lam   : introduce Π
    app   : eliminate Π
    plam  : introduce Path  —  Γ, i:I ⊢ t : A  ⟹  Γ ⊢ ⟨i⟩t : Path A t[i:=0] t[i:=1]
    papp  : eliminate Path  —  t : Path A a b  ⟹  t @ r : A

  Face connection:
    The face lattice tells us *when* a boundary holds (eq0 i / eq1 i).
    `FaceFormula.eq0_iff_env_false` / `eq1_iff_env_true` (below) classify
    which environments put us on the corresponding endpoint.  The
    boundary reduction itself is now an NbE theorem in `Readback.lean`
    (`readback_papp_plam`); the previous step-level path β `PathWitness`
    encoding has been removed alongside its underlying axiom.

  ## Universe-aware shape

  Contexts pair each binder with a `Σ ℓ : ULevel, CType ℓ` so individual
  bindings can live at any universe level.  `HasType` is universe-aware
  via an implicit `{ℓ : ULevel}` parameter on the type slot — each
  judgement Γ ⊢ t : A carries the level of A as the implicit ℓ.  Each
  constructor's CType references take their own level (some constructors
  bind two distinct levels for domain and codomain).
-/

import CubicalTransport.DimLine

-- ── Context ───────────────────────────────────────────────────────────────────

/-- A level-tagged CType bundle: pairs a CType with its universe level. -/
abbrev CTypeAny := Σ ℓ : ULevel, CType ℓ

/-- Typing context: ordered list of `(name, ⟨ℓ, A⟩)` bindings.  Each
    binder lives at its own universe level. -/
abbrev Ctx := List (String × CTypeAny)

-- ── Typing judgment ───────────────────────────────────────────────────────────

/-- The typing judgment  Γ ⊢ t : A.  Universe-aware: A's level lives at
    the implicit `{ℓ : ULevel}` slot. -/
inductive HasType : Ctx → CTerm → ∀ {ℓ : ULevel}, CType ℓ → Prop where
  | var  {Γ : Ctx} {x : String} {ℓ : ULevel} {A : CType ℓ} :
           (x, ⟨ℓ, A⟩) ∈ Γ →
           HasType Γ (.var x) A

  | lam  {Γ : Ctx} {x : String} {ℓ ℓ' : ULevel}
         {A : CType ℓ} {B : CType ℓ'} {t : CTerm} {var : String} :
           HasType ((x, ⟨ℓ, A⟩) :: Γ) t B →
           HasType Γ (.lam x t) (.pi var A B)

  | app  {Γ : Ctx} {ℓ ℓ' : ULevel}
         {A : CType ℓ} {B : CType ℓ'} {f a : CTerm} {var : String} :
           HasType Γ f (.pi var A B) →
           HasType Γ a A →
           HasType Γ (.app f a) B

  /-- Path introduction: ⟨i⟩t has type  Path A t[i:=0] t[i:=1].
      The boundaries are computed directly from substDim. -/
  | plam {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {t : CTerm} {i : DimVar} :
           HasType Γ t A →
           HasType Γ (.plam i t) (.path A (t.substDim i .zero) (t.substDim i .one))

  /-- Path elimination: applying a path to any DimExpr gives the fibration type. -/
  | papp {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {t : CTerm}
         {a b : CTerm} {r : DimExpr} :
           HasType Γ t (.path A a b) →
           HasType Γ (.papp t r) A

  /-- Transport: if t has the type at the 0-end of line L,
      then transpⁱ (λi.A) φ t has the type at the 1-end.
      L packages the binder and body; we unpack to CTerm.transp's raw form. -/
  | transp {Γ : Ctx} {ℓ : ULevel} {t : CTerm} {φ : FaceFormula} :
             (L : DimLine ℓ) →
             HasType Γ t L.at0 →
             HasType Γ (.transp L.binder L.body φ t) L.at1

  /-- Composition: compⁱ (λi.A) φ u t has type L.at1, given:
      · t : L.at0                       (base term)
      · u : L.at1                       (system body typed at output end)
      · on (φ ∩ i=0), u[i:=0] = t      (compatibility side-condition)

      The compat condition has the universally-quantified shape
          ∀ env, φ.eval env = true → env i = false → u[i:=0] = t
      which is logically equivalent to
          (∃ env, φ ∧ i=0) → u[i:=0] = t
      — i.e. *if the face (φ ∩ i=0) is actually inhabited, the equation holds*.
      This makes `.bot`-faced systems (unsatisfiable) vacuously compatible while
      still forcing the equation wherever the face can actually be met.

      The face formula φ and system body u are stored raw (no System wrapper)
      to avoid a circular import; System.lean wraps these for ergonomics. -/
  | comp {Γ : Ctx} {ℓ : ULevel} {t u : CTerm} {φ : FaceFormula} :
           (L : DimLine ℓ) →
           HasType Γ t L.at0 →
           HasType Γ u L.at1 →
           (∀ env : DimVar → Bool,
              φ.eval env = true → env L.binder = false →
              CTerm.substDimBool L.binder false u = t) →
           HasType Γ (.comp L.binder L.body φ u t) L.at1

  /-- Σ introduction: pairing.  Non-dependent form — `B` does not depend
      on the first component's value. -/
  | pair {Γ : Ctx} {ℓ ℓ' : ULevel}
         {A : CType ℓ} {B : CType ℓ'} {a b : CTerm} {var : String} :
           HasType Γ a A →
           HasType Γ b B →
           HasType Γ (.pair a b) (.sigma var A B)

  /-- Σ elimination (first projection). -/
  | fst  {Γ : Ctx} {ℓ ℓ' : ULevel}
         {A : CType ℓ} {B : CType ℓ'} {t : CTerm} {var : String} :
           HasType Γ t (.sigma var A B) →
           HasType Γ (.fst t) A

  /-- Σ elimination (second projection). -/
  | snd  {Γ : Ctx} {ℓ ℓ' : ULevel}
         {A : CType ℓ} {B : CType ℓ'} {t : CTerm} {var : String} :
           HasType Γ t (.sigma var A B) →
           HasType Γ (.snd t) B

  /-- Schema constructor application (REL1 minimal-viable typing).

      Asserts that `.ctor S c params args` has type `.ind S params`.
      No premises constrain `args` here — the per-argument typing
      against `S.ctors[c].args` is enforced at runtime by `eval` and
      the boundary system, not at the typing-judgement level.  REL2
      will refine this to a fully dependent rule with one premise per
      `CtorSpec.args` entry.

      Result level `ℓ` is user-specified at the type level (matching
      `CType.ind`'s explicit level annotation). -/
  | ctor {Γ : Ctx} {ℓ : ULevel} {S : CTypeSchema}
         {params : List (Σ ℓ' : ULevel, CType ℓ')} {c : String} {args : List CTerm} :
           HasType Γ (.ctor S c params args) (CType.ind (ℓ := ℓ) S params)

  /-- Inductive eliminator (REL1 minimal-viable, *non-dependent* form).

      The motive is treated as a function `.pi (.ind S params) C` for
      some closed `C : CType` (constant motive), so the eliminator's
      result type is `C`.  Dependent motives — where `C` varies with
      the eliminated value — are deferred to REL2.

      Branch-level coherence (each branch body matches its ctor's
      curried signature, including recursive-arg hypotheses for `.self`
      args) is checked at runtime by `eval`, not statically here. -/
  | indElim {Γ : Ctx} {ℓ ℓ' : ULevel} {S : CTypeSchema}
            {params : List (Σ ℓ'' : ULevel, CType ℓ'')}
            {motive target : CTerm} {branches : List (String × CTerm)}
            {C : CType ℓ'} {var : String} :
              HasType Γ target (CType.ind (ℓ := ℓ) S params) →
              HasType Γ motive (.pi var (CType.ind (ℓ := ℓ) S params) C) →
              HasType Γ (.indElim S params motive branches target) C

  /-- Dimension expression lifted to the term language.

      Pre-REL2 (`Dev_REL1`) typed `.dimExpr r` at the placeholder
      `.univ`.  REL2 promotes the cubical interval to a first-class
      CType (`CType.interval`) and types `.dimExpr r : .interval`.
      Path-constructor dim arguments now carry real semantic ground:
      `loop @ r`, `seg @ r`, `squash _ _ @ r`, etc. all type-check
      against the corresponding `.dim` arg position. -/
  | dimExpr {Γ : Ctx} {r : DimExpr} : HasType Γ (.dimExpr r) .interval

  /-- Typing rule for `code`: `code A` has type `.univ (ℓ := ℓ)` where
      `A : CType ℓ`.  The dual elimination rule is `CType.El`, whose
      reduction `El (code A) = A` is the universe-code β-rule. -/
  | code  : ∀ {Γ : Ctx} {ℓ : ULevel} (A : CType ℓ),
            HasType Γ (.code A) (.univ (ℓ := ℓ))

-- ── Structural rules ──────────────────────────────────────────────────────────

/-- Core: insert (x, B) into context Γ between a prefix Γ₁ and suffix Γ₂.
    We take `Γ` as a free variable and carry `Γ = Γ₁ ++ Γ₂` as a hypothesis
    so that `induction h` works (the index must be a variable). -/
private theorem HasType.weaken_core
    (x : String) {ℓB : ULevel} (B : CType ℓB) (Γ₂ : Ctx)
    {Γ : Ctx} {t : CTerm} {ℓ : ULevel} {A : CType ℓ}
    (h : HasType Γ t A) :
    ∀ (Γ₁ : Ctx), Γ = Γ₁ ++ Γ₂ → HasType (Γ₁ ++ (x, ⟨ℓB, B⟩) :: Γ₂) t A := by
  induction h with
  | var mem =>
      intro Γ₁ hΓ; subst hΓ
      apply HasType.var
      rw [List.mem_append] at mem ⊢
      rcases mem with h | h
      · exact Or.inl h
      · exact Or.inr (List.mem_cons.mpr (Or.inr h))
  | lam ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.lam (ih ((_, _) :: Γ₁) rfl)
  | app hf ha ihf iha =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.app (ihf Γ₁ rfl) (iha Γ₁ rfl)
  | plam ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.plam (ih Γ₁ rfl)
  | papp ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.papp (ih Γ₁ rfl)
  | transp L ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.transp L (ih Γ₁ rfl)
  | comp L ht hu hc iht ihu =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.comp L (iht Γ₁ rfl) (ihu Γ₁ rfl) hc
  | pair ha hb iha ihb =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.pair (iha Γ₁ rfl) (ihb Γ₁ rfl)
  | fst ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.fst (ih Γ₁ rfl)
  | snd ht ih =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.snd (ih Γ₁ rfl)
  | ctor =>
      intro _ _; exact HasType.ctor
  | indElim ht hm iht ihm =>
      intro Γ₁ hΓ; subst hΓ
      exact HasType.indElim (iht Γ₁ rfl) (ihm Γ₁ rfl)
  | dimExpr =>
      intro _ _; exact HasType.dimExpr
  | code A =>
      intro _ _; exact HasType.code A

theorem HasType.weaken (x : String) {ℓB : ULevel} (B : CType ℓB)
    {Γ : Ctx} {t : CTerm} {ℓ : ULevel} {A : CType ℓ}
    (h : HasType Γ t A) : HasType ((x, ⟨ℓB, B⟩) :: Γ) t A :=
  HasType.weaken_core x B Γ h [] rfl

-- ── Face lattice connection ───────────────────────────────────────────────────
-- These lemmas tie the Bool-valued face semantics to the dimensional endpoints.

namespace FaceFormula

/-- The face (i=0) holds precisely when env i = false. -/
theorem eq0_iff_env_false (i : DimVar) (env : DimVar → Bool) :
    (eq0 i).eval env = true ↔ env i = false := by
  simp [eval]

/-- The face (i=1) holds precisely when env i = true. -/
theorem eq1_iff_env_true (i : DimVar) (env : DimVar → Bool) :
    (eq1 i).eval env = true ↔ env i = true := by
  simp [eval]

end FaceFormula

-- ── Typing inversion ─────────────────────────────────────────────────────────

/-- Inversion for plam: if ⟨i⟩t : Path A a b, then t : A and
    the boundaries are exactly the substDim images. -/
theorem HasType.plam_inv
    (Γ : Ctx) (i : DimVar) (t : CTerm) {ℓ : ULevel} (A : CType ℓ) (a b : CTerm)
    (h : HasType Γ (.plam i t) (.path A a b)) :
    HasType Γ t A ∧
    a = t.substDim i .zero ∧
    b = t.substDim i .one := by
  cases h with
  | plam ht => exact ⟨ht, rfl, rfl⟩

/-- Inversion for papp: if t @ r : A, then t : Path A a b for some a b. -/
theorem HasType.papp_inv
    (Γ : Ctx) (t : CTerm) (r : DimExpr) {ℓ : ULevel} (A : CType ℓ)
    (h : HasType Γ (.papp t r) A) :
    ∃ a b, HasType Γ t (.path A a b) := by
  cases h with
  | papp ht => exact ⟨_, _, ht⟩

/-- Inversion for comp: reading off all components of a composition judgment.
    We return an existential DimLine to avoid the naming clash between the
    outer parameter and the constructor's internal binder. -/
theorem HasType.comp_inv
    (Γ : Ctx) (i : DimVar) {ℓ : ULevel} (bodyA : CType ℓ) (φ : FaceFormula)
    (u t : CTerm) (A : CType ℓ)
    (h : HasType Γ (.comp i bodyA φ u t) A) :
    ∃ L : DimLine ℓ, L.binder = i ∧ L.body = bodyA ∧
      A = L.at1 ∧
      HasType Γ t L.at0 ∧
      HasType Γ u L.at1 ∧
      (∀ env : DimVar → Bool,
          φ.eval env = true → env L.binder = false →
          CTerm.substDimBool L.binder false u = t) := by
  cases h with
  | comp L ht hu hc => exact ⟨L, rfl, rfl, rfl, ht, hu, hc⟩

/-- Inversion for transp: the output type is exactly L.at1. -/
theorem HasType.transp_inv
    (Γ : Ctx) (i : DimVar) {ℓ : ULevel} (bodyA : CType ℓ) (φ : FaceFormula)
    (t : CTerm) (A : CType ℓ)
    (h : HasType Γ (.transp i bodyA φ t) A) :
    ∃ L : DimLine ℓ, L.binder = i ∧ L.body = bodyA ∧
      A = L.at1 ∧ HasType Γ t L.at0 := by
  cases h with
  | transp L ht => exact ⟨L, rfl, rfl, rfl, ht⟩