b9ca1d8875
Some checks are pending
Lean Action CI / build (push) Waiting to run
Per THEORY.md §3.1: cubical-native modal type formers as the engine
support layer for the cohesive modality triple (ʃ ⊣ ♭ ⊣ ♯).
CType (3 level-preserving formers):
· CType.flat / .sharp / .shape : {ℓ} → CType ℓ → CType ℓ
CTerm (6 — three intros + three elims, modelled on .glueIn / .unglue):
· CTerm.flatIntro / .sharpIntro / .shapeIntro : CTerm → CTerm
· CTerm.flatElim / .sharpElim / .shapeElim : CTerm → CTerm → CTerm
Cascade: Syntax (constructors + SkeletalCType + skeleton + substDim);
DecEq (beq arms); Subst (substDim / substDimExpr + 6 rfl theorems);
DimLine (cascade through 8 dim-absent / dim-substitution lemma families);
Value (3 vIntro CVal + 3 nElim CNeu); Eval (β-reduction axioms +
stuck-neutral propagation, "marker neutral" idiom from vFst/vSnd
preserved); Readback (3 vIntro + 3 nElim arms with axioms); Typing
(6 HasType cases — bare recursion-principle shape; modal cohesion
dependent-motive form deferred to Phase 3); Reflect (3 reflectCType + 6
reflectCTerm + 3 reifyCType with level-coherence discharge + 6
reifyCTerm); Question (6 modal arms + 6 IsModalLine classifier
predicates with their Decidable instances); FFITest (cval/cterm
summary arms).
No Rust changes (Phase 2). No Modal.lean module (Phase 3). No
Crisp / CContext.crispVar / cohesive_triple theorems (Phase 3).
Build: lake build (48 jobs) + lake build CubicalTransport (42 jobs) PASS.
+664 lines across 11 files, 0 removed, 0 new sorries.
Honest deferrals documented:
· Modal type-formers do not yet reduce under transport/comp; the
match A blocks have wildcards so transp i (flat A) φ t produces a
stuck ntransp neutral (correct under current axiom set; cohesion-
driven reductions land in Phase 3).
· HasType.flatElim et al carry the bare recursion-principle shape;
the cohesive-HoTT-correct dependent-motive form requires the modal
predicate lattice from Phase 3.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
364 lines
16 KiB
Text
364 lines
16 KiB
Text
/-
|
||
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 (ℓ := ℓ))
|
||
|
||
/-- **Modal introduction (flat).** Given `a : A`, the term
|
||
`flatIntro a` inhabits `flat A`. Engine-layer rule —
|
||
modal-cohesion contextual restrictions (Crisp variables,
|
||
Π-modality interaction, etc.) land in Phase 3. -/
|
||
| flatIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
|
||
HasType Γ a A →
|
||
HasType Γ (.flatIntro a) (.flat A)
|
||
|
||
/-- **Modal introduction (sharp).** -/
|
||
| sharpIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
|
||
HasType Γ a A →
|
||
HasType Γ (.sharpIntro a) (.sharp A)
|
||
|
||
/-- **Modal introduction (shape).** -/
|
||
| shapeIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
|
||
HasType Γ a A →
|
||
HasType Γ (.shapeIntro a) (.shape A)
|
||
|
||
/-- **Modal elimination (flat).** Given an eliminator `f : A → C`
|
||
and a scrutinee `m : flat A`, produce a term of type `C`.
|
||
|
||
Engine layer: this is the bare recursion-principle shape; the
|
||
modal-cohesion side-conditions (e.g. C must be flat-modal for
|
||
the elim to be well-formed in cohesive HoTT) are deferred to
|
||
Phase 3 (`Modal.lean`). At the engine layer the rule reflects
|
||
the recursion principle directly so that `eval` and `readback`
|
||
can dispatch on it. -/
|
||
| flatElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
|
||
{f m : CTerm} {var : String} :
|
||
HasType Γ f (.pi var A C) →
|
||
HasType Γ m (.flat A) →
|
||
HasType Γ (.flatElim f m) C
|
||
|
||
/-- **Modal elimination (sharp).** -/
|
||
| sharpElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
|
||
{f m : CTerm} {var : String} :
|
||
HasType Γ f (.pi var A C) →
|
||
HasType Γ m (.sharp A) →
|
||
HasType Γ (.sharpElim f m) C
|
||
|
||
/-- **Modal elimination (shape).** -/
|
||
| shapeElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
|
||
{f m : CTerm} {var : String} :
|
||
HasType Γ f (.pi var A C) →
|
||
HasType Γ m (.shape A) →
|
||
HasType Γ (.shapeElim f m) C
|
||
|
||
-- ── 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
|
||
| flatIntro ha ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.flatIntro (ih Γ₁ rfl)
|
||
| sharpIntro ha ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.sharpIntro (ih Γ₁ rfl)
|
||
| shapeIntro ha ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.shapeIntro (ih Γ₁ rfl)
|
||
| flatElim hf hm ihf ihm =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.flatElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
|
||
| sharpElim hf hm ihf ihm =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.sharpElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
|
||
| shapeElim hf hm ihf ihm =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.shapeElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
|
||
|
||
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⟩
|