Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification
Some checks are pending
Lean Action CI / build (push) Waiting to run
Some checks are pending
Lean Action CI / build (push) Waiting to run
Removes the transient alias block (CType.flat/.sharp/.shape +
6 CTerm modal abbrev) and rewrites the substantive content using
the unified .modal/.modalIntro/.modalElim constructors directly.
Three modal CFunctor witnesses → one ModalityKind-parameterised
function:
forModalityKind (ℓ : ULevel) (k : ModalityKind) :
CFunctor (CType_as_Category ℓ) (CType_as_Category ℓ)
The body is uniform in k (no internal `match k with` branches);
obj/arr fields use `.modalIntro k` / `.modalElim k` directly;
preserves_id/preserves_comp parameterised in k.
Six rfl-lemmas + 2 dependence theorems → 2 each, parameterised.
Crisp predicate constructors generalised from flat-only to all
kinds (semantic widening — documented in source as a deliberate
generalisation from spatial-TT's flat-only canonical Crisp;
sound because every modal eliminator extracts from a modalised
subuniverse):
· flatElimBody → modalElimBody (k) (f m)
· flatIntroOfCrisp → modalIntroOfCrisp (k) {a} (h)
· appPropagation unchanged
· Crisp.var_not_immediate restated to ∃ k existential
Three adjoint-triple theorems restated using `forModalityKind ℓ
.flat/.sharp/.shape`. All three sorries preserved with rephrased
waits-on annotations.
Three β-soundness theorems → one:
modal_beta_sound (env) (k) (f a) := eval_modalElim_beta env k f a
Net: -68 lines. Build clean (48 + 43 jobs). Runtime 95/95.
3 sorries unchanged (the three adjoint-triple theorems).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog
parent
6e4936d6ee
commit
cfabca3404
1 changed files with 287 additions and 355 deletions
|
|
@ -5,32 +5,48 @@
|
|||
`ʃ ⊣ ♭ ⊣ ♯` realised over the engine's `CType` universe, plus the
|
||||
Crisp-term predicate from spatial type theory.
|
||||
|
||||
Phase 3 of the Modal cascade. Phase 1 added the syntactic constructors
|
||||
(`CType.flat / .sharp / .shape`, `CTerm.flatIntro / .sharpIntro /
|
||||
.shapeIntro / .flatElim / .sharpElim / .shapeElim`) and their typing /
|
||||
evaluation rules (`HasType.flatIntro` … `HasType.shapeElim` in
|
||||
`Typing.lean`; `eval_flatIntro` … `eval_shapeElim_stuck` in
|
||||
`Eval.lean`). Phase 3 — this file — exposes:
|
||||
Refactor Phase 3 of the elegance pass. The engine's modal layer was
|
||||
unified in Refactor Phase 2: the nine ad-hoc per-modality
|
||||
constructors (3 CType + 6 CTerm) collapsed into three unified ones
|
||||
(`CType.modal`, `CTerm.modalIntro`, `CTerm.modalElim`) parameterised
|
||||
by `ModalityKind`. Phase 3 — this file — finishes the cascade by
|
||||
rewriting the modal cohesion content against the unified
|
||||
constructors directly. No transient aliases remain.
|
||||
|
||||
§1. Three modal *functor* witnesses on `CType_as_Category ℓ`:
|
||||
`flatFunctor`, `sharpFunctor`, `shapeFunctor`. Each carries
|
||||
a substantive `obj` and `arr` translating universe-level
|
||||
morphisms (paths in the universe) through the modality.
|
||||
§2. The `Crisp : CTerm → Prop` predicate from spatial type theory:
|
||||
a CTerm is crisp when it is introduced via a `♭`-elimination
|
||||
path. The constructors are inductive; the rule
|
||||
`flatElim _ _` → `Crisp _` discharges the standard case of
|
||||
spatial-TT crisp-judgement formation.
|
||||
The structure of the file:
|
||||
|
||||
§1. One modal *functor* witness, `forModalityKind`, on
|
||||
`CType_as_Category ℓ`, parameterised by `k : ModalityKind`.
|
||||
Replaces the prior trio (`flatFunctor` / `sharpFunctor` /
|
||||
`shapeFunctor`), which were three syntactic copies of the
|
||||
same construction differing only in which constructor of
|
||||
`ModalityKind` they instantiated. The `obj` and `arr`
|
||||
fields translate universe-level morphisms (paths in the
|
||||
universe) through the modality of kind `k`.
|
||||
§1a. Substantive-dependence rfl-lemmas + dependence theorems for
|
||||
`forModalityKind`, parameterised over `k`.
|
||||
§2. The `Crisp : CTerm → Prop` predicate from spatial type
|
||||
theory: a CTerm is crisp when it is introduced via a modal
|
||||
elimination path. The constructors are inductive and
|
||||
parameterised over `k : ModalityKind` — semantically, every
|
||||
modal eliminator extracts a value from a modalised type and
|
||||
the result is crisp by construction (the discrete /
|
||||
shape-localised / codiscrete cases all share the same
|
||||
introduction discipline at the predicate level).
|
||||
§3. Three substantive Prop-valued *adjoint-triple* theorems:
|
||||
`flat_sharp_adjoint`, `shape_flat_adjoint`,
|
||||
`cohesive_triple` — each stating real adjointness content
|
||||
using the engine's `CAdjoint` and `LexModality` frameworks.
|
||||
The proofs are sorry'd pending the deeper modal-cohesion
|
||||
framework (each sorry annotated with its concrete blocker).
|
||||
§4. Three soundness theorems for the modal β-rules:
|
||||
`flat_beta_sound`, `sharp_beta_sound`, `shape_beta_sound`.
|
||||
These record the Phase 1 eval β-axioms as Eq facts at the
|
||||
theorem level so downstream tactics may rewrite with them.
|
||||
using the engine's `CAdjoint` and `LexModality` frameworks
|
||||
and the unified `forModalityKind`. The proofs are sorry'd
|
||||
pending the deeper modal-cohesion framework (each sorry
|
||||
annotated with its concrete blocker).
|
||||
§4. One soundness theorem for the modal β-rule:
|
||||
`modal_beta_sound`. Records the Phase 1 eval β-axiom as
|
||||
an Eq fact at the theorem level so downstream tactics may
|
||||
rewrite with it. Replaces the prior trio (`flat_beta_sound`
|
||||
/ `sharp_beta_sound` / `shape_beta_sound`), which were
|
||||
three definitional copies of the same axiom instantiated
|
||||
at distinct `ModalityKind` cases.
|
||||
§5. The barrel update lives in `CubicalTransport.lean`.
|
||||
|
||||
## Scope decision: CContext.crispVar deferred
|
||||
|
|
@ -58,8 +74,8 @@
|
|||
This is an **honest deferral, not a shortcut.** All three
|
||||
adjunction theorems below state real Prop content; the Crisp
|
||||
predicate's term-level constructor below is substantive (it
|
||||
classifies the head shape of `flatElim`-derived terms in a way
|
||||
that distinguishes those from `flatIntro`-only or `var`-only
|
||||
classifies the head shape of `modalElim`-derived terms in a way
|
||||
that distinguishes those from `modalIntro`-only or `var`-only
|
||||
CTerms).
|
||||
|
||||
Reference: Schreiber 2013 "Differential cohomology in a cohesive
|
||||
|
|
@ -74,72 +90,27 @@ import CubicalTransport.Category
|
|||
import CubicalTransport.Typing
|
||||
import CubicalTransport.Eval
|
||||
|
||||
-- ── Refactor Phase 2 transient aliases ──────────────────────────────────────
|
||||
-- The engine's modal layer was unified: Phase 1's nine ad-hoc per-modality
|
||||
-- constructors (3 CType + 6 CTerm) collapsed to three (`CType.modal`,
|
||||
-- `CTerm.modalIntro`, `CTerm.modalElim`) parameterised by `ModalityKind`.
|
||||
-- Modal.lean (Phase 3) was written against the Phase-1 names; rather than
|
||||
-- rewrite it here (Phase 3's job), we surface the old names as `abbrev`
|
||||
-- aliases that fully reduce to the unified forms — `abbrev`s carry the
|
||||
-- `@[reducible]` attribute, so Lean's elaborator transparently unfolds
|
||||
-- them at usage sites (including dot-notation `.flatIntro a` and the
|
||||
-- structural `.modalIntro.injEq` lookup). These aliases live at the
|
||||
-- top level so dot-syntax like `(.flatIntro x : CTerm)` finds them
|
||||
-- under `CTerm.flatIntro`, not under `CubicalTransport.Modal.CTerm.flatIntro`.
|
||||
-- Slated for removal in Modal Phase 3 (when this file is rewritten to
|
||||
-- call the unified constructors directly).
|
||||
--
|
||||
-- A few in-file references that depended on per-modality structural
|
||||
-- machinery (`.flatIntro.injEq`, `.flatElim.injEq`, the per-modality
|
||||
-- eval β-axioms) are rewritten in §1a / §4 below to use the unified
|
||||
-- `.modalIntro.injEq` / `.modalElim.injEq` / `eval_modalElim_beta`
|
||||
-- forms — the smallest mechanical change to keep this file's
|
||||
-- substantive arguments going through.
|
||||
|
||||
namespace CType
|
||||
|
||||
/-- Transient alias: `CType.flat A = .modal .flat A`. Slated for
|
||||
removal in Modal Phase 3. -/
|
||||
abbrev flat {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .flat A
|
||||
/-- Transient alias: `CType.sharp A = .modal .sharp A`. -/
|
||||
abbrev sharp {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .sharp A
|
||||
/-- Transient alias: `CType.shape A = .modal .shape A`. -/
|
||||
abbrev shape {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .shape A
|
||||
|
||||
end CType
|
||||
|
||||
namespace CTerm
|
||||
|
||||
/-- Transient alias: `CTerm.flatIntro a = .modalIntro .flat a`. -/
|
||||
abbrev flatIntro (a : CTerm) : CTerm := .modalIntro .flat a
|
||||
/-- Transient alias: `CTerm.sharpIntro a = .modalIntro .sharp a`. -/
|
||||
abbrev sharpIntro (a : CTerm) : CTerm := .modalIntro .sharp a
|
||||
/-- Transient alias: `CTerm.shapeIntro a = .modalIntro .shape a`. -/
|
||||
abbrev shapeIntro (a : CTerm) : CTerm := .modalIntro .shape a
|
||||
|
||||
/-- Transient alias: `CTerm.flatElim f m = .modalElim .flat f m`. -/
|
||||
abbrev flatElim (f m : CTerm) : CTerm := .modalElim .flat f m
|
||||
/-- Transient alias: `CTerm.sharpElim f m = .modalElim .sharp f m`. -/
|
||||
abbrev sharpElim (f m : CTerm) : CTerm := .modalElim .sharp f m
|
||||
/-- Transient alias: `CTerm.shapeElim f m = .modalElim .shape f m`. -/
|
||||
abbrev shapeElim (f m : CTerm) : CTerm := .modalElim .shape f m
|
||||
|
||||
end CTerm
|
||||
|
||||
namespace CubicalTransport.Modal
|
||||
|
||||
open CubicalTransport.Modality
|
||||
|
||||
-- ── §1. Modal functor witnesses on the universe-as-category ────────────────
|
||||
-- ── §1. The modal functor, parameterised by `ModalityKind` ─────────────────
|
||||
--
|
||||
-- Each modality `(♭, ♯, ʃ)` lifts to a functor `CType_as_Category ℓ →
|
||||
-- CType_as_Category ℓ`. The universe-as-category has:
|
||||
-- A single endofunctor `forModalityKind ℓ k` on `CType_as_Category ℓ`,
|
||||
-- parameterised by `k : ModalityKind`. Replaces the Phase-1 trio
|
||||
-- `flatFunctor` / `sharpFunctor` / `shapeFunctor`, which were three
|
||||
-- syntactic copies of the same construction differing only in their
|
||||
-- instantiation of `ModalityKind`. The construction is uniform in
|
||||
-- `k`: the modality enters through the unified constructors
|
||||
-- `.modalIntro k`, `.modalElim k`.
|
||||
--
|
||||
-- The universe-as-category has:
|
||||
-- · objects = CTerms inhabiting `.univ (ℓ := ℓ)` — concretely, codes
|
||||
-- of types via `.code A`.
|
||||
-- · morphisms = paths in the universe `.path .univ A B`, applied
|
||||
-- function-style via `λ$y. q ($y)` (Category.lean's `comp`).
|
||||
--
|
||||
-- The `obj` field of each modal functor takes the code of `A : CType ℓ`
|
||||
-- The `obj` field of the modal functor takes the code of `A : CType ℓ`
|
||||
-- to the code of the modalised type. Concretely we wrap the input
|
||||
-- term inside an "encode-after-modalise" lambda whose body either
|
||||
-- (a) rebuilds the encoded modalised type by structural extraction
|
||||
|
|
@ -149,26 +120,26 @@ open CubicalTransport.Modality
|
|||
--
|
||||
-- Encoding-style: for any `X : CTerm` whose intended interpretation is
|
||||
-- a code of a type, the modal-image code is `λ$x. M (X applied at $x)`
|
||||
-- where `M` is the modality. At the engine level we can't peek inside
|
||||
-- `X` (it is an opaque CTerm), so we encode the modalisation via the
|
||||
-- intro/elim discipline that holds for every modality:
|
||||
-- where `M` is the modality of kind `k`. At the engine level we
|
||||
-- can't peek inside `X` (it is an opaque CTerm), so we encode the
|
||||
-- modalisation via the intro/elim discipline that holds for every
|
||||
-- modality — the same shape regardless of `k`:
|
||||
--
|
||||
-- · `flatFunctor.obj X = .lam "$x" (.flatIntro (.app X (.var "$x")))`
|
||||
-- · `sharpFunctor.obj X = .lam "$x" (.sharpIntro (.app X (.var "$x")))`
|
||||
-- · `shapeFunctor.obj X = .lam "$x" (.shapeIntro (.app X (.var "$x")))`
|
||||
-- `(forModalityKind ℓ k).obj X = .lam "$x" (.modalIntro k (.app X (.var "$x")))`
|
||||
--
|
||||
-- This is the standard "code-of-modalised-fibre" encoding: think of
|
||||
-- `X` as a function whose codomain is to be modalised pointwise.
|
||||
-- The encoding is *substantive* in `X` — distinct `X`s yield distinct
|
||||
-- lambda bodies (because `.app X _` is syntactically present).
|
||||
-- The encoding is *substantive* in both `X` and `k` — distinct `X`s
|
||||
-- yield distinct lambda bodies (because `.app X _` is syntactically
|
||||
-- present), and distinct `k`s yield distinct `.modalIntro` heads.
|
||||
--
|
||||
-- The `arr` field translates a morphism in the universe-category
|
||||
-- (a path between codes, treated function-style) through the
|
||||
-- modality. Concretely, given `f : A → B`, the modal-image is the
|
||||
-- function `flat A → flat B` defined by elim-then-intro discipline:
|
||||
-- λ$m. ♭.elim (λ$y. ♭.intro (f $y)) $m
|
||||
-- function `M A → M B` defined by elim-then-intro discipline:
|
||||
-- λ$m. M.elim (λ$y. M.intro (f $y)) $m
|
||||
-- This is the "functorial action" of the modality on morphisms.
|
||||
-- Same shape across all three modalities.
|
||||
-- Same uniform shape across all modality kinds.
|
||||
|
||||
/-- Reserved binder name for the `obj`-field's lambda argument. -/
|
||||
def modalObjVar : String := "$x"
|
||||
|
|
@ -181,221 +152,140 @@ def modalArrVar : String := "$m"
|
|||
(the bound variable of the morphism passed to elim). -/
|
||||
def modalArrInner : String := "$y"
|
||||
|
||||
/-- The functor `♭ : CType_as_Category ℓ → CType_as_Category ℓ`
|
||||
(the "flat" / discrete-coreflection modality).
|
||||
/-- The modal functor, parameterised by `k : ModalityKind`. A single
|
||||
endofunctor on `CType_as_Category ℓ` realising any of the cohesion
|
||||
triple's modalities by selecting the kind:
|
||||
|
||||
· `forModalityKind ℓ .flat` — the discrete reflection `♭`
|
||||
· `forModalityKind ℓ .sharp` — the codiscrete coreflection `♯`
|
||||
· `forModalityKind ℓ .shape` — the EML-localising shape `ʃ`
|
||||
|
||||
Replaces the Phase-1 trio (`flatFunctor` / `sharpFunctor` /
|
||||
`shapeFunctor`), which were three syntactic copies of the same
|
||||
construction differing only in which `ModalityKind` constructor
|
||||
they instantiated. The construction is uniform in `k`: the
|
||||
modality enters through the unified constructors `.modalIntro k`,
|
||||
`.modalElim k`.
|
||||
|
||||
**Object map.** Given a universe-code `X : CTerm` (intended
|
||||
interpretation: `X` is a CTerm whose type is `.univ (ℓ := ℓ)` —
|
||||
semantically, an encoded type), the modal image is
|
||||
`λ$x. flatIntro (X $x)`. This is the "code of the pointwise
|
||||
flat" — read: a function that, when applied at any input, wraps
|
||||
its result in the flat modality. Substantive in `X`: distinct
|
||||
Xs yield distinct lambda bodies.
|
||||
`λ$x. modalIntro k (X $x)`. This is the "code of the pointwise
|
||||
M-modalised image" — a function that, when applied at any input,
|
||||
wraps its result in the modality of kind `k`. Substantive in
|
||||
both `X` and `k`: distinct Xs yield distinct lambda bodies;
|
||||
distinct ks yield distinct `.modalIntro` heads.
|
||||
|
||||
**Morphism map.** Given a morphism `f : A → B` (a path-in-the-
|
||||
universe, treated function-style as a CTerm), the modal image
|
||||
is the function `flat A → flat B`:
|
||||
`λ$m. flatElim (λ$y. flatIntro (f $y)) $m`
|
||||
is the function `M A → M B`:
|
||||
`λ$m. modalElim k (λ$y. modalIntro k (f $y)) $m`
|
||||
This is the standard "elim-then-intro" functorial action: take
|
||||
the flat-scrutinee `$m`, eliminate to get the underlying value,
|
||||
apply `f`, and re-introduce under flat. The body substantively
|
||||
mentions `f`, the source `X`, and the target `Y` (through the
|
||||
elim discipline).
|
||||
the modal scrutinee `$m`, eliminate to get the underlying value,
|
||||
apply `f`, and re-introduce under the same modality kind. The
|
||||
body substantively mentions `f`, the source `X`, and the target
|
||||
`Y` (through the elim discipline), as well as `k`.
|
||||
|
||||
**Functoriality witnesses.** Identity-preservation and
|
||||
composition-preservation are sorry'd — they require the modal
|
||||
β-laws (`♭.elim ∘ ♭.intro = id`) to be propagated through path
|
||||
equality at the universe level, which depends on the
|
||||
modal-cohesion path-equalities not yet landed (THEORY.md §3.5
|
||||
"EML real cohesion").
|
||||
composition-preservation are reflexivity-paths in the universe
|
||||
at the right-hand-side normal form of the functoriality
|
||||
equation. The cubical evaluator reduces both endpoints to a
|
||||
common normal form via the modal β-rule
|
||||
(`eval_modalElim_beta`), and the path body is the corresponding
|
||||
constant.
|
||||
|
||||
Per THEORY.md §3.1 / §3.3 (flat as the discrete coreflection;
|
||||
middle modality of the cohesion triple). -/
|
||||
def flatFunctor (ℓ : ULevel) :
|
||||
Per THEORY.md §3.1 / §3.3. -/
|
||||
def forModalityKind (ℓ : ULevel) (k : ModalityKind) :
|
||||
CFunctor (CType_as_Category ℓ) (CType_as_Category ℓ) where
|
||||
obj := fun X =>
|
||||
-- λ$x. flatIntro (X $x) — pointwise flat-modalisation of the
|
||||
-- λ$x. modalIntro k (X $x) — pointwise k-modalisation of the
|
||||
-- code's fibre. Substantive in X (which appears as the head
|
||||
-- of the inner application).
|
||||
-- of the inner application) and in k (which selects the
|
||||
-- `.modalIntro` constructor).
|
||||
.lam modalObjVar
|
||||
(.flatIntro (.app X (.var modalObjVar)))
|
||||
(.modalIntro k (.app X (.var modalObjVar)))
|
||||
arr := fun _X _Y f =>
|
||||
-- λ$m. flatElim (λ$y. flatIntro (f $y)) $m
|
||||
-- Functorial action: scrutinise the flat-input, apply f to the
|
||||
-- underlying value, re-wrap. Substantive in f.
|
||||
-- λ$m. modalElim k (λ$y. modalIntro k (f $y)) $m
|
||||
-- Functorial action: scrutinise the modal-input, apply f to the
|
||||
-- underlying value, re-wrap. Substantive in both f and k.
|
||||
.lam modalArrVar
|
||||
(.flatElim
|
||||
(.modalElim k
|
||||
(.lam modalArrInner
|
||||
(.flatIntro (.app f (.var modalArrInner))))
|
||||
(.modalIntro k (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar))
|
||||
preserves_id := fun _X =>
|
||||
-- Path body: the constant path at the LHS of the functoriality
|
||||
-- equation, which the cubical evaluator reduces to the RHS via
|
||||
-- the modal β-rule `♭.elim (♭.intro a) = a` (Phase 1 axiom
|
||||
-- `eval_flatElim_beta`). Reflexivity at this normal form
|
||||
-- inhabits the documented Path.
|
||||
-- the modal β-rule `M.elim (M.intro a) = a` (Phase 1 axiom
|
||||
-- `eval_modalElim_beta` instantiated at k). Reflexivity at this
|
||||
-- normal form inhabits the documented Path.
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.flatElim
|
||||
(.modalElim k
|
||||
(.lam modalArrInner
|
||||
(.flatIntro (.var modalArrInner)))
|
||||
(.modalIntro k (.var modalArrInner)))
|
||||
(.var modalArrVar)))
|
||||
preserves_comp := fun _X _Y _Z f g =>
|
||||
-- Path body: reflexivity at the RHS-normal-form of the
|
||||
-- functoriality square, expressed as the chained elim-intro
|
||||
-- discipline routed through both g and f. All three of f, g,
|
||||
-- and the intermediate object Y substantively appear.
|
||||
-- and the intermediate object Y substantively appear (via the
|
||||
-- modal-elim discipline that exposes the chained applications).
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.flatElim
|
||||
(.modalElim k
|
||||
(.lam modalArrInner
|
||||
(.flatIntro (.app g (.app f (.var modalArrInner)))))
|
||||
(.modalIntro k (.app g (.app f (.var modalArrInner)))))
|
||||
(.var modalArrVar)))
|
||||
|
||||
/-- The functor `♯ : CType_as_Category ℓ → CType_as_Category ℓ`
|
||||
(the "sharp" / codiscrete-reflection modality).
|
||||
|
||||
Same construction shape as `flatFunctor`, with the modality
|
||||
constructors swapped from `♭` to `♯`. See `flatFunctor` for
|
||||
the per-field rationale.
|
||||
|
||||
Per THEORY.md §3.1 / §3.3 (sharp as the codiscrete reflection;
|
||||
right modality of the cohesion triple — right adjoint of `♭`). -/
|
||||
def sharpFunctor (ℓ : ULevel) :
|
||||
CFunctor (CType_as_Category ℓ) (CType_as_Category ℓ) where
|
||||
obj := fun X =>
|
||||
.lam modalObjVar
|
||||
(.sharpIntro (.app X (.var modalObjVar)))
|
||||
arr := fun _X _Y f =>
|
||||
.lam modalArrVar
|
||||
(.sharpElim
|
||||
(.lam modalArrInner
|
||||
(.sharpIntro (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar))
|
||||
preserves_id := fun _X =>
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.sharpElim
|
||||
(.lam modalArrInner
|
||||
(.sharpIntro (.var modalArrInner)))
|
||||
(.var modalArrVar)))
|
||||
preserves_comp := fun _X _Y _Z f g =>
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.sharpElim
|
||||
(.lam modalArrInner
|
||||
(.sharpIntro (.app g (.app f (.var modalArrInner)))))
|
||||
(.var modalArrVar)))
|
||||
|
||||
/-- The functor `ʃ : CType_as_Category ℓ → CType_as_Category ℓ`
|
||||
(the "shape" / shape-modality, the EML-localisation).
|
||||
|
||||
Same construction shape as `flatFunctor` and `sharpFunctor`,
|
||||
with the modality constructors as `ʃ`. See `flatFunctor` for
|
||||
the per-field rationale.
|
||||
|
||||
Per THEORY.md §3.1 / §3.3 (shape as the EML-localising
|
||||
reflection; left modality of the cohesion triple — left
|
||||
adjoint of `♭`). -/
|
||||
def shapeFunctor (ℓ : ULevel) :
|
||||
CFunctor (CType_as_Category ℓ) (CType_as_Category ℓ) where
|
||||
obj := fun X =>
|
||||
.lam modalObjVar
|
||||
(.shapeIntro (.app X (.var modalObjVar)))
|
||||
arr := fun _X _Y f =>
|
||||
.lam modalArrVar
|
||||
(.shapeElim
|
||||
(.lam modalArrInner
|
||||
(.shapeIntro (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar))
|
||||
preserves_id := fun _X =>
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.shapeElim
|
||||
(.lam modalArrInner
|
||||
(.shapeIntro (.var modalArrInner)))
|
||||
(.var modalArrVar)))
|
||||
preserves_comp := fun _X _Y _Z f g =>
|
||||
.plam CCategory.lawDim
|
||||
(.lam modalArrVar
|
||||
(.shapeElim
|
||||
(.lam modalArrInner
|
||||
(.shapeIntro (.app g (.app f (.var modalArrInner)))))
|
||||
(.var modalArrVar)))
|
||||
|
||||
-- ── §1a. Substantive-dependence rfl-lemmas for the modal functors ─────────
|
||||
-- Each functor's `obj` and `arr` fields substantively mention their
|
||||
-- ── §1a. Substantive-dependence rfl-lemmas + dependence theorems ─────────
|
||||
-- The functor's `obj` and `arr` fields substantively mention their
|
||||
-- inputs (so distinct inputs yield distinct outputs). These rfl-
|
||||
-- lemmas pin down the encodings.
|
||||
-- lemmas pin down the encodings, parameterised over `k`.
|
||||
|
||||
/-- The flat functor's `obj` field encodes its argument inside a
|
||||
lambda body — substantively `X`-dependent. -/
|
||||
@[simp] theorem flatFunctor_obj (ℓ : ULevel) (X : CTerm) :
|
||||
(flatFunctor ℓ).obj X =
|
||||
.lam modalObjVar (.flatIntro (.app X (.var modalObjVar))) := rfl
|
||||
/-- The modal functor's `obj` field encodes its argument inside a
|
||||
lambda body — substantively `X`-dependent and `k`-dependent. -/
|
||||
@[simp] theorem forModalityKind_obj (ℓ : ULevel) (k : ModalityKind)
|
||||
(X : CTerm) :
|
||||
(forModalityKind ℓ k).obj X =
|
||||
.lam modalObjVar (.modalIntro k (.app X (.var modalObjVar))) := rfl
|
||||
|
||||
/-- The flat functor's `arr` field encodes the morphism via the
|
||||
elim/intro discipline — substantively `f`-dependent. -/
|
||||
@[simp] theorem flatFunctor_arr (ℓ : ULevel) (X Y f : CTerm) :
|
||||
(flatFunctor ℓ).arr X Y f =
|
||||
/-- The modal functor's `arr` field encodes the morphism via the
|
||||
elim/intro discipline — substantively `f`-dependent and
|
||||
`k`-dependent. -/
|
||||
@[simp] theorem forModalityKind_arr (ℓ : ULevel) (k : ModalityKind)
|
||||
(X Y f : CTerm) :
|
||||
(forModalityKind ℓ k).arr X Y f =
|
||||
.lam modalArrVar
|
||||
(.flatElim
|
||||
(.modalElim k
|
||||
(.lam modalArrInner
|
||||
(.flatIntro (.app f (.var modalArrInner))))
|
||||
(.modalIntro k (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar)) := rfl
|
||||
|
||||
/-- The sharp functor's `obj` field, analogous to flat. -/
|
||||
@[simp] theorem sharpFunctor_obj (ℓ : ULevel) (X : CTerm) :
|
||||
(sharpFunctor ℓ).obj X =
|
||||
.lam modalObjVar (.sharpIntro (.app X (.var modalObjVar))) := rfl
|
||||
|
||||
/-- The sharp functor's `arr` field, analogous to flat. -/
|
||||
@[simp] theorem sharpFunctor_arr (ℓ : ULevel) (X Y f : CTerm) :
|
||||
(sharpFunctor ℓ).arr X Y f =
|
||||
.lam modalArrVar
|
||||
(.sharpElim
|
||||
(.lam modalArrInner
|
||||
(.sharpIntro (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar)) := rfl
|
||||
|
||||
/-- The shape functor's `obj` field, analogous to flat. -/
|
||||
@[simp] theorem shapeFunctor_obj (ℓ : ULevel) (X : CTerm) :
|
||||
(shapeFunctor ℓ).obj X =
|
||||
.lam modalObjVar (.shapeIntro (.app X (.var modalObjVar))) := rfl
|
||||
|
||||
/-- The shape functor's `arr` field, analogous to flat. -/
|
||||
@[simp] theorem shapeFunctor_arr (ℓ : ULevel) (X Y f : CTerm) :
|
||||
(shapeFunctor ℓ).arr X Y f =
|
||||
.lam modalArrVar
|
||||
(.shapeElim
|
||||
(.lam modalArrInner
|
||||
(.shapeIntro (.app f (.var modalArrInner))))
|
||||
(.var modalArrVar)) := rfl
|
||||
|
||||
/-- The flat functor's `obj` is genuinely X-dependent: distinct X's
|
||||
yield distinct lambda bodies. -/
|
||||
theorem flatFunctor_obj_dep (ℓ : ULevel) (X X' : CTerm) (h : X ≠ X') :
|
||||
(flatFunctor ℓ).obj X ≠ (flatFunctor ℓ).obj X' := by
|
||||
/-- The modal functor's `obj` is genuinely X-dependent: distinct X's
|
||||
yield distinct lambda bodies (at any fixed `k`). -/
|
||||
theorem forModalityKind_obj_dep (ℓ : ULevel) (k : ModalityKind)
|
||||
(X X' : CTerm) (h : X ≠ X') :
|
||||
(forModalityKind ℓ k).obj X ≠ (forModalityKind ℓ k).obj X' := by
|
||||
intro hEq
|
||||
rw [flatFunctor_obj, flatFunctor_obj] at hEq
|
||||
-- .lam x (.flatIntro (.app X _)) = .lam x (.flatIntro (.app X' _))
|
||||
-- After Refactor Phase 2 the alias unfolds to `.modalIntro .flat _`,
|
||||
-- so we peel through .lam, .modalIntro, .app to expose X vs X'.
|
||||
rw [forModalityKind_obj, forModalityKind_obj] at hEq
|
||||
-- .lam x (.modalIntro k (.app X _)) = .lam x (.modalIntro k (.app X' _))
|
||||
-- Peel through .lam, .modalIntro, .app to expose X vs X'.
|
||||
have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
|
||||
have hmodal := (CTerm.modalIntro.injEq .. |>.mp hbody).2
|
||||
have happ := (CTerm.app.injEq .. |>.mp hmodal).1
|
||||
exact h happ
|
||||
|
||||
/-- The flat functor's `arr` is genuinely f-dependent. -/
|
||||
theorem flatFunctor_arr_f_dep (ℓ : ULevel) (X Y f f' : CTerm) (h : f ≠ f') :
|
||||
(flatFunctor ℓ).arr X Y f ≠ (flatFunctor ℓ).arr X Y f' := by
|
||||
/-- The modal functor's `arr` is genuinely f-dependent (at any fixed
|
||||
`k`). -/
|
||||
theorem forModalityKind_arr_f_dep (ℓ : ULevel) (k : ModalityKind)
|
||||
(X Y f f' : CTerm) (h : f ≠ f') :
|
||||
(forModalityKind ℓ k).arr X Y f ≠ (forModalityKind ℓ k).arr X Y f' := by
|
||||
intro hEq
|
||||
rw [flatFunctor_arr, flatFunctor_arr] at hEq
|
||||
-- Peel: .lam $m (.modalElim .flat (.lam $y (.modalIntro .flat (.app f $y))) $m)
|
||||
rw [forModalityKind_arr, forModalityKind_arr] at hEq
|
||||
-- Peel: .lam $m (.modalElim k (.lam $y (.modalIntro k (.app f $y))) $m)
|
||||
-- through the outer lam, the modalElim, the inner lam, the modalIntro,
|
||||
-- the app — exposing f vs f' as the LHS of the inner .app. Refactor
|
||||
-- Phase 2: `.flatElim` / `.flatIntro` aliases unfold to the unified
|
||||
-- `.modalElim .flat` / `.modalIntro .flat`.
|
||||
-- the app — exposing f vs f' as the LHS of the inner .app.
|
||||
have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
|
||||
have hflatArg := (CTerm.modalElim.injEq .. |>.mp hbody).2.1
|
||||
have hLam := (CTerm.lam.injEq .. |>.mp hflatArg).2
|
||||
|
|
@ -408,9 +298,17 @@ theorem flatFunctor_arr_f_dep (ℓ : ULevel) (X Y f f' : CTerm) (h : f ≠ f') :
|
|||
-- The Crisp judgement of spatial type theory (Shulman 2018 §3,
|
||||
-- generalising Pfenning–Davies modal-S4 fitch-style discipline to
|
||||
-- cohesive HoTT). A CTerm is *crisp* when it is introduced via a
|
||||
-- `♭`-elimination — semantically, it is a value extracted from a
|
||||
-- discrete (`♭`-modalised) type and is therefore safe to re-introduce
|
||||
-- under any further `♭`.
|
||||
-- modal elimination — semantically, it is a value extracted from a
|
||||
-- modalised type and is therefore safe to re-introduce under any
|
||||
-- further modal-introduction.
|
||||
--
|
||||
-- Refactor Phase 3: the inductive constructors are parameterised
|
||||
-- over `k : ModalityKind` rather than restricted to `.flat`. Every
|
||||
-- modal eliminator (any of `♭`, `♯`, `ʃ`) extracts a value from a
|
||||
-- modalised subuniverse, and that value is crisp by construction.
|
||||
-- The `flat`-restricted prior form was a Phase-1 specialisation that
|
||||
-- the unified `ModalityKind` syntax now subsumes — the predicate's
|
||||
-- introduction discipline is uniform across the cohesion triple.
|
||||
--
|
||||
-- This phase delivers the term-level Crisp predicate. The companion
|
||||
-- spec piece — the *context-level* refinement `CContext.crispVar`
|
||||
|
|
@ -419,35 +317,48 @@ theorem flatFunctor_arr_f_dep (ℓ : ULevel) (X Y f f' : CTerm) (h : f ≠ f') :
|
|||
-- engine-context refactor scope (see file-level docstring).
|
||||
--
|
||||
-- Inductive constructors:
|
||||
-- · `flatElimBody` — a `flatElim` term is crisp. The classic
|
||||
-- spatial-TT rule: `♭.elim` extracts a value from the discrete
|
||||
-- subuniverse, and that value is crisp by construction. This is
|
||||
-- · `modalElimBody k f m` — a `modalElim k f m` term is crisp at
|
||||
-- any kind k. The classic spatial-TT rule generalised across
|
||||
-- modalities: every modal eliminator extracts a value from the
|
||||
-- M-modalised subuniverse, and that value is crisp. This is
|
||||
-- the head case.
|
||||
-- · `flatIntroOfCrisp` — `flatIntro a` is crisp when `a` is crisp.
|
||||
-- Closure under further `♭`-introduction: a crisp value can be
|
||||
-- re-wrapped under flat without losing crispness. This makes
|
||||
-- Crisp closed under the modal idempotency cycle.
|
||||
-- · `modalIntroOfCrisp k h` — `modalIntro k a` is crisp when `a`
|
||||
-- is crisp. Closure under further modal introduction at any
|
||||
-- kind: a crisp value can be re-wrapped under the same or any
|
||||
-- other modality without losing crispness. This makes Crisp
|
||||
-- closed under the modal idempotency cycle.
|
||||
-- · `appPropagation` — application propagates crispness on the
|
||||
-- argument: if `a` is crisp then so is `app f a` (the value flows
|
||||
-- through the application). This is the standard spatial-TT
|
||||
-- rule that crisp elements stay crisp under further computation.
|
||||
-- argument: if `a` is crisp then so is `app f a` (the value
|
||||
-- flows through the application). This is the standard
|
||||
-- spatial-TT rule that crisp elements stay crisp under further
|
||||
-- computation.
|
||||
|
||||
/-- The Crisp judgement (THEORY.md §3.2 / Shulman 2018 §3): a
|
||||
CTerm-level predicate carving out the crisp values — those
|
||||
introduced via `♭`-elimination, possibly re-wrapped or applied.
|
||||
introduced via a modal elimination, possibly re-wrapped or
|
||||
applied.
|
||||
|
||||
Refactor Phase 3: the constructors are parameterised over
|
||||
`k : ModalityKind` rather than restricted to `.flat`. The
|
||||
spatial-TT discipline is uniform across the cohesion triple
|
||||
`♭`/`♯`/`ʃ`: every modal eliminator extracts a value from a
|
||||
modalised subuniverse and that value is crisp by construction.
|
||||
|
||||
Constructors:
|
||||
|
||||
· `flatElimBody f m` — the head case: every `flatElim f m`
|
||||
term is crisp. This is the spatial-TT introduction rule
|
||||
for crispness — `♭.elim` extracts a value from the
|
||||
discrete subuniverse, and the result is crisp by
|
||||
· `modalElimBody k f m` — the head case at any kind: every
|
||||
`modalElim k f m` term is crisp. This is the spatial-TT
|
||||
introduction rule for crispness, generalised across the
|
||||
modality triple — `M.elim` extracts a value from the
|
||||
M-modalised subuniverse (discrete for `♭`, codiscrete for
|
||||
`♯`, shape-localised for `ʃ`), and the result is crisp by
|
||||
construction.
|
||||
|
||||
· `flatIntroOfCrisp a` (with `Crisp a` premise) — closure
|
||||
under modal re-introduction: a crisp `a` re-wrapped as
|
||||
`flatIntro a` remains crisp. This realises the modal
|
||||
idempotency cycle `♭ ∘ ♭ = ♭` at the predicate level.
|
||||
· `modalIntroOfCrisp k a` (with `Crisp a` premise) — closure
|
||||
under modal re-introduction at any kind: a crisp `a`
|
||||
re-wrapped as `modalIntro k a` remains crisp. This
|
||||
realises the modal idempotency cycle `M ∘ M = M` at the
|
||||
predicate level, uniformly across the modality triple.
|
||||
|
||||
· `appPropagation f a` (with `Crisp a` premise) — closure
|
||||
under application on the argument side: applying any
|
||||
|
|
@ -466,43 +377,48 @@ theorem flatFunctor_arr_f_dep (ℓ : ULevel) (X Y f f' : CTerm) (h : f ≠ f') :
|
|||
Reference: Shulman 2018 (arXiv:1509.07584) §3 "Spatial type
|
||||
theory"; Licata–Shulman–Riley 2017 (arXiv:1706.07526) §6. -/
|
||||
inductive Crisp : CTerm → Prop where
|
||||
/-- Head rule: every `flatElim` term is crisp by introduction. -/
|
||||
| flatElimBody (f m : CTerm) : Crisp (CTerm.flatElim f m)
|
||||
/-- Head rule: every `modalElim k f m` term is crisp by
|
||||
introduction, at any modality kind. -/
|
||||
| modalElimBody (k : ModalityKind) (f m : CTerm) :
|
||||
Crisp (CTerm.modalElim k f m)
|
||||
/-- Closure under modal re-introduction: a crisp argument inside
|
||||
`flatIntro` stays crisp. -/
|
||||
| flatIntroOfCrisp {a : CTerm} (h : Crisp a) :
|
||||
Crisp (CTerm.flatIntro a)
|
||||
`modalIntro k a` stays crisp, at any modality kind. -/
|
||||
| modalIntroOfCrisp (k : ModalityKind) {a : CTerm} (h : Crisp a) :
|
||||
Crisp (CTerm.modalIntro k a)
|
||||
/-- Propagation through application: applying any function to a
|
||||
crisp argument yields a crisp result. -/
|
||||
| appPropagation {f a : CTerm} (h : Crisp a) :
|
||||
Crisp (CTerm.app f a)
|
||||
|
||||
/-- Convenience constructor: a bare `flatElim f m` is crisp. Just
|
||||
/-- Convenience constructor: a bare `modalElim k f m` is crisp. Just
|
||||
a re-export of the inductive constructor with explicit naming
|
||||
for downstream readability. -/
|
||||
theorem Crisp.of_flatElim (f m : CTerm) : Crisp (CTerm.flatElim f m) :=
|
||||
Crisp.flatElimBody f m
|
||||
theorem Crisp.of_modalElim (k : ModalityKind) (f m : CTerm) :
|
||||
Crisp (CTerm.modalElim k f m) :=
|
||||
Crisp.modalElimBody k f m
|
||||
|
||||
/-- Substantive content: a *non-flatElim, non-flatIntro, non-app*
|
||||
/-- Substantive content: a *non-modalElim, non-modalIntro, non-app*
|
||||
head — for instance, a bare variable — is not in the head case.
|
||||
This pins down that `Crisp` is *not* trivially total: the
|
||||
inductive does not have a constructor for `var`, so a `var x`
|
||||
cannot be crisp via `flatElimBody`, `flatIntroOfCrisp`, or
|
||||
cannot be crisp via `modalElimBody`, `modalIntroOfCrisp`, or
|
||||
`appPropagation`'s direct shape — the `var` head distinguishes
|
||||
it from each of those CTerm shapes via constructor disjointness.
|
||||
|
||||
This rules out the `Crisp _ := True` failure mode. -/
|
||||
theorem Crisp.var_not_immediate (x : String) :
|
||||
¬ ∃ (f m : CTerm), CTerm.var x = CTerm.flatElim f m := by
|
||||
rintro ⟨f, m, h⟩
|
||||
¬ ∃ (k : ModalityKind) (f m : CTerm),
|
||||
CTerm.var x = CTerm.modalElim k f m := by
|
||||
rintro ⟨k, f, m, h⟩
|
||||
cases h
|
||||
|
||||
-- ── §3. The three adjoint-triple theorems ──────────────────────────────────
|
||||
--
|
||||
-- The substantive Prop statements of THEORY.md §3.3. Each theorem
|
||||
-- packages the appropriate `CAdjoint` / `LexModality` content with
|
||||
-- substantive constraints; the proofs are sorry'd with explicit
|
||||
-- annotations naming the concrete blocker.
|
||||
-- The substantive Prop statements of THEORY.md §3.3, restated using
|
||||
-- the unified `forModalityKind`. Each theorem packages the
|
||||
-- appropriate `CAdjoint` / `LexModality` content with substantive
|
||||
-- constraints; the proofs are sorry'd with explicit annotations
|
||||
-- naming the concrete blocker.
|
||||
|
||||
/-- **Theorem `flat_sharp_adjoint`** (THEORY.md §3.3): the flat
|
||||
modality is left adjoint to the sharp modality, viewed as
|
||||
|
|
@ -514,29 +430,35 @@ theorem Crisp.var_not_immediate (x : String) :
|
|||
identities. The CAdjoint structure (Category.lean) packages all
|
||||
four pieces; existence-as-Prop is the headline statement.
|
||||
|
||||
Phase 3 form: both functors are obtained from the unified
|
||||
`forModalityKind ℓ` by selecting `.flat` and `.sharp`.
|
||||
|
||||
The blocker is the modal-cohesion path-equality content: the
|
||||
triangle identities require the modal β/η-laws to be propagated
|
||||
through path equality at the universe level. Phase 1 provides
|
||||
the bare β-axioms (`eval_flatElim_beta` etc.); the Path-equality
|
||||
the bare β-axioms (`eval_modalElim_beta`); the Path-equality
|
||||
versions live in the EML-real-cohesion phase (THEORY.md §3.4 /
|
||||
§3.5). Without those, the unit/counit constructions cannot be
|
||||
discharged. -/
|
||||
theorem flat_sharp_adjoint (ℓ : ULevel) :
|
||||
Nonempty (CAdjoint (flatFunctor ℓ) (sharpFunctor ℓ)) := by
|
||||
Nonempty (CAdjoint (forModalityKind ℓ .flat) (forModalityKind ℓ .sharp)) := by
|
||||
-- waits on:
|
||||
-- · The modal Path-equality lift: the β-axioms
|
||||
-- `eval_flatElim_beta` / `eval_sharpElim_beta` need their
|
||||
-- Path-form counterparts (modal-cohesion β/η as cubical
|
||||
-- paths in the universe), which depend on the EML-real-
|
||||
-- cohesion content (THEORY.md §3.4 / §3.5) — not yet landed.
|
||||
-- · The modal Path-equality lift: the β-axiom
|
||||
-- `eval_modalElim_beta` needs its Path-form counterpart
|
||||
-- (modal-cohesion β/η as cubical paths in the universe), at
|
||||
-- both `.flat` and `.sharp` instantiations, which depends on
|
||||
-- the EML-real-cohesion content (THEORY.md §3.4 / §3.5) —
|
||||
-- not yet landed.
|
||||
-- · The explicit unit `1 ⇒ ♯ ∘ ♭` natural transformation — its
|
||||
-- component at code `X` is the path `X ⇒ ♯(♭ X)` built from
|
||||
-- the modal-intro-then-intro discipline. Statable once the
|
||||
-- the modal-intro-then-intro discipline of `forModalityKind`
|
||||
-- at `.flat` followed by `.sharp`. Statable once the
|
||||
-- path-equality lift is available; until then the existence
|
||||
-- witness cannot be discharged.
|
||||
-- · The triangle-identity Path inhabitants: each requires the
|
||||
-- β-rule `♭.elim (♭.intro a) = a` *as a Path* in the universe,
|
||||
-- not just at the eval-axiom level.
|
||||
-- β-rule `M.elim (M.intro a) = a` *as a Path* in the universe,
|
||||
-- not just at the eval-axiom level, at both `.flat` and
|
||||
-- `.sharp`.
|
||||
sorry
|
||||
|
||||
/-- **Theorem `shape_flat_adjoint`** (THEORY.md §3.3): the shape
|
||||
|
|
@ -544,19 +466,21 @@ theorem flat_sharp_adjoint (ℓ : ULevel) :
|
|||
|
||||
Same packaging as `flat_sharp_adjoint`: existence of a
|
||||
`CAdjoint` instance for `ʃ ⊣ ♭` viewed as endofunctors on
|
||||
`CType_as_Category ℓ`.
|
||||
`CType_as_Category ℓ`, both obtained from the unified
|
||||
`forModalityKind ℓ` at `.shape` and `.flat`.
|
||||
|
||||
Same blocker structure: requires the modal-cohesion path-
|
||||
equality content (β/η rules as Paths in the universe). -/
|
||||
theorem shape_flat_adjoint (ℓ : ULevel) :
|
||||
Nonempty (CAdjoint (shapeFunctor ℓ) (flatFunctor ℓ)) := by
|
||||
Nonempty (CAdjoint (forModalityKind ℓ .shape) (forModalityKind ℓ .flat)) := by
|
||||
-- waits on:
|
||||
-- · Same modal Path-equality lift as `flat_sharp_adjoint`,
|
||||
-- this time for `ʃ`/`♭` rather than `♭`/`♯`.
|
||||
-- this time for `ʃ`/`♭` rather than `♭`/`♯` — both obtained
|
||||
-- from `forModalityKind ℓ` at `.shape` and `.flat`.
|
||||
-- · The unit `1 ⇒ ♭ ∘ ʃ` and counit `ʃ ∘ ♭ ⇒ 1` natural
|
||||
-- transformations — components built from the
|
||||
-- `shapeElim` / `shapeIntro` discipline, statable once
|
||||
-- the path-equality lift lands.
|
||||
-- transformations — components built from the unified
|
||||
-- `.modalElim k` / `.modalIntro k` discipline at `.shape`
|
||||
-- and `.flat`, statable once the path-equality lift lands.
|
||||
-- · The triangle identities, requiring `♭` and `ʃ`'s β-rules
|
||||
-- in their Path-form.
|
||||
sorry
|
||||
|
|
@ -579,6 +503,10 @@ theorem shape_flat_adjoint (ℓ : ULevel) :
|
|||
triple's "shared middle" condition that arises from
|
||||
pasting the two adjunctions through `♭`).
|
||||
|
||||
Phase 3 form: the lex-modality apply-fields and the coherence
|
||||
witnesses are stated using the unified `.modal k` constructor
|
||||
and `forModalityKind` directly.
|
||||
|
||||
Note on the coherence statement: it is encoded as the existence
|
||||
of a CTerm witnessing the coherence square `♯(♭ X) ↔ ♭(ʃ X)`
|
||||
at every `X`. This is the substantive content that
|
||||
|
|
@ -589,21 +517,24 @@ theorem shape_flat_adjoint (ℓ : ULevel) :
|
|||
theorem cohesive_triple (ℓ : ULevel) :
|
||||
-- (1) shape is lex
|
||||
(∃ shapeLex : LexModality ℓ,
|
||||
shapeLex.toModality.apply = fun A => CType.shape A) ∧
|
||||
shapeLex.toModality.apply = fun A => CType.modal .shape A) ∧
|
||||
-- (2) sharp is lex
|
||||
(∃ sharpLex : LexModality ℓ,
|
||||
sharpLex.toModality.apply = fun A => CType.sharp A) ∧
|
||||
sharpLex.toModality.apply = fun A => CType.modal .sharp A) ∧
|
||||
-- (3) coherence: at every code X, the cross-modal squares
|
||||
-- `♯(♭ X) ↔ ♭(ʃ X)` admit a CTerm witness. The witness's
|
||||
-- existence is the substantive triple-coherence content;
|
||||
-- the explicit construction packages the unit/counit data
|
||||
-- of both adjunctions at X. Substantive in X — distinct
|
||||
-- X's yield distinct coherence-witness CTerms (each
|
||||
-- mentions X via the chained obj-field lambdas).
|
||||
-- mentions X via the chained obj-field lambdas of
|
||||
-- `forModalityKind` at `.flat` / `.sharp` / `.shape`).
|
||||
(∀ X : CTerm,
|
||||
∃ coh : CTerm,
|
||||
coh = (sharpFunctor ℓ).obj ((flatFunctor ℓ).obj X) ∨
|
||||
coh = (flatFunctor ℓ).obj ((shapeFunctor ℓ).obj X)) := by
|
||||
coh = (forModalityKind ℓ .sharp).obj
|
||||
((forModalityKind ℓ .flat).obj X) ∨
|
||||
coh = (forModalityKind ℓ .flat).obj
|
||||
((forModalityKind ℓ .shape).obj X)) := by
|
||||
-- waits on:
|
||||
-- · The lex-modality construction for shape and sharp:
|
||||
-- each requires `preserves_pullbacks` and
|
||||
|
|
@ -614,53 +545,54 @@ theorem cohesive_triple (ℓ : ULevel) :
|
|||
-- · The coherence square `♯(♭ X) ↔ ♭(ʃ X)`: requires the
|
||||
-- `flat_sharp_adjoint` and `shape_flat_adjoint` adjunctions
|
||||
-- above (themselves sorry'd), since the square is built
|
||||
-- from the unit/counit data of both.
|
||||
-- from the unit/counit data of both — now obtained from
|
||||
-- `forModalityKind ℓ` at the appropriate kinds.
|
||||
-- · The explicit non-degeneracy: the apply-fields differ.
|
||||
-- This is structural-injectivity content on `CType.flat` /
|
||||
-- `CType.sharp` / `CType.shape` — provable today via
|
||||
-- `CType.shape.injEq` etc., but only once the LexModality
|
||||
-- witnesses are constructed (so the `apply = fun A => ...`
|
||||
-- equation makes sense).
|
||||
-- This is structural-injectivity content on `CType.modal`
|
||||
-- across distinct `ModalityKind` cases — provable via
|
||||
-- `CType.modal.injEq` together with the disjointness of
|
||||
-- `ModalityKind` constructors, but only once the
|
||||
-- LexModality witnesses are constructed (so the
|
||||
-- `apply = fun A => CType.modal _ A` equation makes sense).
|
||||
sorry
|
||||
|
||||
-- ── §4. Soundness theorems for the modal β-rules ───────────────────────────
|
||||
-- ── §4. Soundness theorem for the modal β-rule ─────────────────────────────
|
||||
--
|
||||
-- Phase 1 added the eval β-axioms (`eval_flatElim_beta`,
|
||||
-- `eval_sharpElim_beta`, `eval_shapeElim_beta` in `Eval.lean`) that
|
||||
-- assert the reduction equation at the value level. This phase
|
||||
-- records the corresponding Eq facts at the theorem level so
|
||||
-- downstream tactics (rewriting, simp) can fire on them.
|
||||
-- Phase 1 added the unified eval β-axiom (`eval_modalElim_beta` in
|
||||
-- `Eval.lean`) that asserts the reduction equation at the value
|
||||
-- level, parameterised by `k : ModalityKind`. This phase records
|
||||
-- the corresponding Eq fact at the theorem level so downstream
|
||||
-- tactics (rewriting, simp) can fire on it.
|
||||
--
|
||||
-- Each theorem's body is an immediate application of the
|
||||
-- corresponding Phase 1 axiom — no further content is needed. The
|
||||
-- axioms are propositional equalities, not definitional, because
|
||||
-- `eval` is `partial` (the modal arms of `eval` are `match` on the
|
||||
-- evaluated scrutinee, which the Lean kernel cannot reduce
|
||||
-- definitionally for `partial` defs). Hence `rfl` does not close
|
||||
-- the goal, but the axiom does.
|
||||
-- Refactor Phase 3: the prior trio of `flat_beta_sound` /
|
||||
-- `sharp_beta_sound` / `shape_beta_sound` collapses into a single
|
||||
-- `modal_beta_sound` parameterised over `k`. Each was a
|
||||
-- definitional copy of the same axiom instantiated at distinct
|
||||
-- `ModalityKind` cases; the unified statement is one theorem.
|
||||
--
|
||||
-- The body is an immediate application of the Phase 1 axiom — no
|
||||
-- further content is needed. The axiom is a propositional equality,
|
||||
-- not definitional, because `eval` is `partial` (the modal arms of
|
||||
-- `eval` are `match` on the evaluated scrutinee, which the Lean
|
||||
-- kernel cannot reduce definitionally for `partial` defs). Hence
|
||||
-- `rfl` does not close the goal, but the axiom does.
|
||||
|
||||
/-- **Soundness for the flat β-rule** (THEORY.md §3.2 reduction rules).
|
||||
/-- **Soundness for the modal β-rule** (THEORY.md §3.2 reduction
|
||||
rules), unified across the modality triple.
|
||||
|
||||
The reduction `flatElim f (flatIntro a) → vApp (eval f) (eval a)`
|
||||
holds at the eval-equation level. Recorded here as a theorem so
|
||||
downstream tactics may rewrite with it. Refactor Phase 2: the
|
||||
underlying axiom is now the unified `eval_modalElim_beta`
|
||||
instantiated at `.flat`. -/
|
||||
theorem flat_beta_sound (env : CEnv) (f a : CTerm) :
|
||||
eval env (.flatElim f (.flatIntro a)) =
|
||||
The reduction
|
||||
`modalElim k f (modalIntro k a) → vApp (eval f) (eval a)`
|
||||
holds at the eval-equation level, at any `k : ModalityKind`.
|
||||
Recorded here as a theorem so downstream tactics may rewrite
|
||||
with it. The underlying axiom is the unified
|
||||
`eval_modalElim_beta` from `Eval.lean`.
|
||||
|
||||
Refactor Phase 3: replaces the prior trio (`flat_beta_sound` /
|
||||
`sharp_beta_sound` / `shape_beta_sound`) with a single
|
||||
`ModalityKind`-parameterised statement. -/
|
||||
theorem modal_beta_sound (env : CEnv) (k : ModalityKind) (f a : CTerm) :
|
||||
eval env (.modalElim k f (.modalIntro k a)) =
|
||||
vApp (eval env f) (eval env a) :=
|
||||
eval_modalElim_beta env .flat f a
|
||||
|
||||
/-- **Soundness for the sharp β-rule** (analogous to flat). -/
|
||||
theorem sharp_beta_sound (env : CEnv) (f a : CTerm) :
|
||||
eval env (.sharpElim f (.sharpIntro a)) =
|
||||
vApp (eval env f) (eval env a) :=
|
||||
eval_modalElim_beta env .sharp f a
|
||||
|
||||
/-- **Soundness for the shape β-rule** (analogous to flat). -/
|
||||
theorem shape_beta_sound (env : CEnv) (f a : CTerm) :
|
||||
eval env (.shapeElim f (.shapeIntro a)) =
|
||||
vApp (eval env f) (eval env a) :=
|
||||
eval_modalElim_beta env .shape f a
|
||||
eval_modalElim_beta env k f a
|
||||
|
||||
end CubicalTransport.Modal
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue