max/cubical-transport-hott-lean4
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

CType inductive-type encoding (for paideia K7 cubical Path) #1

New issue
Open
opened 2026-04-30 15:47:11 -05:00 by max · 0 comments
max commented 2026-04-30 15:47:11 -05:00
Owner
Copy link

Issue 002 — CType inductive-type encoding for K7's full cubical Path

Status: open · Filed by: paideia, 2026-04-30 · Activated in: another Claude session (engine work)
Repository targeted: cubical-transport-hott-lean4 (the engine)

Summary

Paideia's K7 (BootstrapGradient) currently ships as a discrete
sequence of (MathemaId, MasteryProvenance, Outcome) triples — the
"discrete shadow" of the cubical Path it aspires to be. The
original Eulerian framing was K7 as a literal Path between
successive MasteryProvenance traces, observable as a cubical
object via the engine's transp/comp/Path machinery.

The blocker: the engine's CType algebra has no inductive
types. Available CTypes:

| univ                                 — universe
| pi (A B : CType)                     — function
| path (A : CType) (a b : CTerm)       — path type
| sigma (A B : CType)                  — non-dependent pair
| glue (φ : FaceFormula) (T : CType) … — Glue

No Nat, no List, no Bool, no general inductive families. This
means there is no CType representing "a list of KnowledgeNodes,"
which is what MasteryProvenance := Trace KnowledgeNode needs to be
encoded as.

Without that CType, the engine's Path cannot quantify over
MasteryProvenance endpoints. K7's full cubical encoding is
therefore impossible at the paideia layer with the current engine
API — it requires engine work.

Concrete blocker for paideia

The aspirational shape:

namespace Paideia.Foundation

/-- A K7 BootstrapGradient as a literal cubical path. -/
def CubicalGradient (p₀ p₁ : MasteryProvenance) : Type :=
  CTerm  -- of type (Path A (toCTerm p₀) (toCTerm p₁))

Requires toCTerm : MasteryProvenance → CTerm. No such function
exists or can be defined: the cubical-syntax universe lacks the
inductive structure needed to host a list-of-records value.

The current K7 ships paideia-domain MathPath (see
Paideia/Foundation/K7Cubical.lean) — a typed two-endpoint
structure with interp : Bool → MasteryProvenance and endpoint
conditions. This captures the cubical shape (boundary, reverse,
restricted composition) but is parallel to engine Path, not an
embedding into it.

Suggested engine extension (one option)

Add inductive types to CubicalTransport.Syntax:

inductive CType where
  | univ                                          : CType
  | pi    (A B : CType)                           : CType
  | path  (A : CType) (a b : CTerm)               : CType
  | sigma (A B : CType)                           : CType
  | glue  (φ : FaceFormula) (T : CType) …         : CType
  -- NEW:
  | inductive (name : String)
              (constructors : List (String × CType))
                                                  : CType
  -- or equivalently a list-specific:
  | list  (A : CType)                             : CType

inductive CTerm where
  | …
  -- NEW (for list):
  | nil                                           : CTerm
  | cons   (head tail : CTerm)                    : CTerm
  | listElim (motive nilCase consCase target : CTerm) : CTerm

The full extension would also include:

  • typing rules for the new constructors;
  • substitution / evaluation / readback cases;
  • transp and comp cases (well-typed transport over inductive
    values is a known cubical construction — Cohen et al., CCHM
    §6 covers it for HITs; for plain inductives it's straightforward);
  • soundness theorems matching the existing chapter's discipline.

Alternative: a generic-inductive CType

Rather than adding list (and later nat, bool, etc.) one at a
time, expose a schema for declaring inductive types:

structure CTypeSchema where
  name           : String
  paramTypes     : List CType
  constructors   : List (String × List CType × CType)  -- ctor sigs + return

-- Add a CType constructor that's parameterised by a Schema:
| inductiveBy  (S : CTypeSchema) : CType

This is closer to Lean's own inductive-types-as-data approach.
More upfront work; covers all paideia's future encoding needs in
one move.

Cost

Substantial — not a single-file refactor. The engine's
CubicalTransport.{Syntax, Subst, Typing, Eval, Value, Readback, Transport, TransportLaws, CompLaws, Soundness} modules each gain
new cases for the new constructors. Estimated: one to two
"chapters" of CCHM-style implementation. Comparable in scope to
the existing Glue chapter, which took its own development cycle.

Benefit

  • K7's literal cubical encoding becomes possible. Paideia's
    MathPath can be retired in favour of a typed CTerm of
    cubical-Path type, with engine transp/comp operating over
    the bootstrap trajectory directly.
  • Downstream cubical applications gain encoding power. Any
    future project that wants to model Lean-inductive data inside
    the cubical universe (provenance traces, EML rendering inputs,
    arbitrary curated structures) gets a uniform encoding path.
  • The engine becomes self-sufficient for HIT-flavoured
    development.     Higher inductive types are the natural next step
    after this foundation.

Compatibility note for the Claude session that picks this up

Paideia depends on the engine. This refactor would not break
existing paideia code (no current K-hypothesis uses inductive
CTypes), but would enable paideia to retire MathPath in favour
of an engine-grounded version. The migration sequence:

  1. Land the engine refactor on a feature branch.
  2. Add an import CubicalTransport.Inductive (or whatever) to
    paideia's K7Cubical.
  3. Define MasteryProvenance.toCTerm using the new constructors.
  4. Define CubicalGradient as a CTerm-typed value.
  5. Prove the bridge: paideia's MathPath p₀ p₁ is equivalent to
    CTerms of type Path MPCType (p₀.toCTerm) (p₁.toCTerm).
  6. Update paideia's K7Cubical to use the engine version under the
    hood, keeping the user-facing API identical.

If the engine refactor is too large to coordinate, a partial
refactor — adding only list (the minimum for Trace's shape) —
is acceptable. Paideia's needs are bounded; the schema-based
generalisation is a nice-to-have, not a blocker.

Pre-built reference

Paideia/Foundation/K7Cubical.lean contains the paideia-side
MathPath structure with the operations (const, reverse,
comp-on-reflexive-paths, transport) the engine version would
mirror. The proofs there are paideia-specific but the signatures
are the API the engine version should expose to consumers — the
literal CTerm encoding can be wired in behind the same external
shape.

Filed from paideia/docs/issues/002-cterm-inductive-encoding.md @ commit 01f1e2b

# Issue 002 — `CType` inductive-type encoding for K7's full cubical Path **Status:** open · **Filed by:** paideia, 2026-04-30 · **Activated in:** another Claude session (engine work) **Repository targeted:** `cubical-transport-hott-lean4` (the engine) ## Summary Paideia's K7 (`BootstrapGradient`) currently ships as a *discrete* sequence of `(MathemaId, MasteryProvenance, Outcome)` triples — the "discrete shadow" of the cubical Path it aspires to be. The original Eulerian framing was K7 as a literal `Path` between successive `MasteryProvenance` traces, observable as a cubical object via the engine's `transp`/`comp`/`Path` machinery. **The blocker:** the engine's `CType` algebra has no inductive types. Available `CType`s: ``` | univ — universe | pi (A B : CType) — function | path (A : CType) (a b : CTerm) — path type | sigma (A B : CType) — non-dependent pair | glue (φ : FaceFormula) (T : CType) … — Glue ``` No `Nat`, no `List`, no `Bool`, no general inductive families. This means there is **no `CType` representing "a list of `KnowledgeNode`s,"** which is what `MasteryProvenance := Trace KnowledgeNode` needs to be encoded as. Without that `CType`, the engine's `Path` cannot quantify over `MasteryProvenance` endpoints. K7's full cubical encoding is therefore impossible at the *paideia* layer with the current engine API — it requires engine work. ## Concrete blocker for paideia The aspirational shape: ```lean namespace Paideia.Foundation /-- A K7 BootstrapGradient as a literal cubical path. -/ def CubicalGradient (p₀ p₁ : MasteryProvenance) : Type := CTerm -- of type (Path A (toCTerm p₀) (toCTerm p₁)) ``` Requires `toCTerm : MasteryProvenance → CTerm`. No such function exists or can be defined: the cubical-syntax universe lacks the inductive structure needed to host a list-of-records value. The current K7 ships paideia-domain `MathPath` (see `Paideia/Foundation/K7Cubical.lean`) — a typed two-endpoint structure with `interp : Bool → MasteryProvenance` and endpoint conditions. This captures the cubical *shape* (boundary, reverse, restricted composition) but is parallel to engine `Path`, not an embedding into it. ## Suggested engine extension (one option) Add inductive types to `CubicalTransport.Syntax`: ```lean inductive CType where | univ : CType | pi (A B : CType) : CType | path (A : CType) (a b : CTerm) : CType | sigma (A B : CType) : CType | glue (φ : FaceFormula) (T : CType) … : CType -- NEW: | inductive (name : String) (constructors : List (String × CType)) : CType -- or equivalently a list-specific: | list (A : CType) : CType inductive CTerm where | … -- NEW (for list): | nil : CTerm | cons (head tail : CTerm) : CTerm | listElim (motive nilCase consCase target : CTerm) : CTerm ``` The full extension would also include: - typing rules for the new constructors; - substitution / evaluation / readback cases; - `transp` and `comp` cases (well-typed transport over inductive values is a known cubical construction — Cohen et al., CCHM §6 covers it for HITs; for plain inductives it's straightforward); - soundness theorems matching the existing chapter's discipline. ## Alternative: a generic-inductive `CType` Rather than adding `list` (and later `nat`, `bool`, etc.) one at a time, expose a *schema* for declaring inductive types: ```lean structure CTypeSchema where name : String paramTypes : List CType constructors : List (String × List CType × CType) -- ctor sigs + return -- Add a CType constructor that's parameterised by a Schema: | inductiveBy (S : CTypeSchema) : CType ``` This is closer to Lean's own inductive-types-as-data approach. More upfront work; covers all paideia's future encoding needs in one move. ## Cost Substantial — not a single-file refactor. The engine's `CubicalTransport.{Syntax, Subst, Typing, Eval, Value, Readback, Transport, TransportLaws, CompLaws, Soundness}` modules each gain new cases for the new constructors. Estimated: one to two "chapters" of CCHM-style implementation. Comparable in scope to the existing `Glue` chapter, which took its own development cycle. ## Benefit - **K7's literal cubical encoding becomes possible.** Paideia's `MathPath` can be retired in favour of a typed `CTerm` of cubical-Path type, with engine `transp`/`comp` operating over the bootstrap trajectory directly. - **Downstream cubical applications gain encoding power.** Any future project that wants to model Lean-inductive data inside the cubical universe (provenance traces, EML rendering inputs, arbitrary curated structures) gets a uniform encoding path. - **The engine becomes self-sufficient for HIT-flavoured development.** Higher inductive types are the natural next step after this foundation. ## Compatibility note for the Claude session that picks this up Paideia depends on the engine. This refactor would not break existing paideia code (no current K-hypothesis uses inductive CTypes), but would *enable* paideia to retire `MathPath` in favour of an engine-grounded version. The migration sequence: 1. Land the engine refactor on a feature branch. 2. Add an `import CubicalTransport.Inductive` (or whatever) to paideia's `K7Cubical`. 3. Define `MasteryProvenance.toCTerm` using the new constructors. 4. Define `CubicalGradient` as a `CTerm`-typed value. 5. Prove the bridge: paideia's `MathPath p₀ p₁` is equivalent to `CTerm`s of type `Path MPCType (p₀.toCTerm) (p₁.toCTerm)`. 6. Update paideia's K7Cubical to use the engine version under the hood, keeping the user-facing API identical. If the engine refactor is too large to coordinate, a partial refactor — adding only `list` (the minimum for `Trace`'s shape) — is acceptable. Paideia's needs are bounded; the schema-based generalisation is a nice-to-have, not a blocker. ## Pre-built reference `Paideia/Foundation/K7Cubical.lean` contains the paideia-side `MathPath` structure with the operations (`const`, `reverse`, `comp`-on-reflexive-paths, `transport`) the engine version would mirror. The proofs there are paideia-specific but the *signatures* are the API the engine version should expose to consumers — the literal CTerm encoding can be wired in behind the same external shape. --- Filed from paideia/docs/issues/002-cterm-inductive-encoding.md @ commit 01f1e2b
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
Dev_REL2
Dev_REL1
No results found.
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: max/cubical-transport-hott-lean4#1
No description provided.
Delete branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?