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

/-
  Topolei.Cubical.Typing
  ======================
  The typing judgment  Γ ⊢ t : A  for the cubical term language.

  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.

  Note: Π types are non-dependent here (B is a CType, not CTerm → CType).
  Dependent Π is deferred until we have a term evaluator.
-/

import CubicalTransport.DimLine

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

/-- Typing context: ordered list of term-variable bindings. -/
abbrev Ctx := List (String × CType)

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

/-- The typing judgment  Γ ⊢ t : A. -/
inductive HasType : Ctx → CTerm → CType → Prop where
  | var  : (x, A) ∈ Γ →
           HasType Γ (.var x) A

  | lam  : HasType ((x, A) :: Γ) t B →
           HasType Γ (.lam x t) (.pi A B)

  | app  : HasType Γ f (.pi 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 : 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 : 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 : (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 : (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 : HasType Γ a A →
           HasType Γ b B →
           HasType Γ (.pair a b) (.sigma A B)

  /-- Σ elimination (first projection). -/
  | fst  : HasType Γ t (.sigma A B) →
           HasType Γ (.fst t) A

  /-- Σ elimination (second projection). -/
  | snd  : HasType Γ t (.sigma A B) →
           HasType Γ (.snd t) B

-- ── 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 : CType) (Γ₂ : Ctx)
    {Γ : Ctx} {t : CTerm} {A : CType}
    (h : HasType Γ t A) :
    ∀ (Γ₁ : Ctx), Γ = Γ₁ ++ Γ₂ → HasType (Γ₁ ++ (x, 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)

theorem HasType.weaken (x : String) (B : CType)
    (h : HasType Γ t A) : HasType ((x, 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) (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) (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) (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) (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⟩