From f9e79b7b0d3ab85db384b0e54ba1d8c5f8a63666 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Thu, 30 Apr 2026 14:57:22 -0600 Subject: [PATCH] REL1: design doc for schema-based inductive + HIT CTypes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Filed against issue #1 (paideia K7 cubical-Path encoding blocker). Generalised scope: full HIT support — point + path constructors with boundary partial-element systems, multi-param schemas, recursive ctor args. CTypeSchema/CtorSpec/CTypeArg embedded in the mutual inductive block alongside CType/CTerm. New constructors: CType.ind, CTerm.{dimExpr, ctor, indElim}, CVal.vctor, CNeu.nIndElim. Tag layout frozen for REL1; Rust ABI bumps 1→2. Topolei migration surveyed and documented (§9.1) — ~150–250 lines across DecEq, Trace, TraceAt, FluxR; Path.lean and EML/Cubical.lean unaffected. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/INDUCTIVE_TYPES.md | 650 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 650 insertions(+) create mode 100644 docs/INDUCTIVE_TYPES.md diff --git a/docs/INDUCTIVE_TYPES.md b/docs/INDUCTIVE_TYPES.md new file mode 100644 index 0000000..f1b6777 --- /dev/null +++ b/docs/INDUCTIVE_TYPES.md @@ -0,0 +1,650 @@ +# INDUCTIVE_TYPES.md — Schema-based inductive & higher-inductive CTypes + +*REL1 design contract for the schema-driven inductive-type extension to +the cubical engine. Targets: full HIT support (point + path +constructors with arbitrary boundary partial-element systems, multi- +parameter schemas, recursive constructor arguments). Filed against +issue #1 in `max/cubical-transport-hott-lean4` (2026-04-30); requested +by paideia for K7's literal cubical-Path encoding.* + +--- + +## 0. Status & scope + +**Status:** REL1 design — landing on `Dev_REL1`, not `main`, until the +whole inductive refactor lands. + +**In scope (REL1):** + +- Plain (point-only) inductives: `Nat`, `Bool`, `List A`, polymorphic + parametric inductives, recursive ctor args. +- HITs: path constructors with `dim`-binders + boundary partial-element + system; supports `S¹`, interval `I`, propositional truncation + `‖A‖₋₁`, suspension `Σ A`, pushouts. +- Eliminator (`indElim`) with motive over `.ind S params`, one branch + per ctor. Branches for path ctors carry a coherence obligation + matching the boundary system. +- Transport / hcomp / heterogeneous comp over `.ind S params`. +- FFI: full Rust dispatch on the new constructor tags. + +**Deferred (post-REL1):** + +- Indexed inductive families (`Vec n`, `Eq` natively). +- Mutual / nested inductives in a single schema. +- Higher path constructors (2-cells / squares / cubes inside a single + ctor body — the "boundary system" mechanism *technically* supports + arbitrarily many `dim` binders, but only in REL2 will we wire the + composition rules end-to-end). +- Quotient inductive-inductive types (QIITs). + +**Breaking changes accepted up-front (REL1 mandate):** + +- `CType` and `CTerm` gain new constructors — every Lean module that + pattern-matches on these (`Subst`, `DimLine`, `Typing`, `Eval`, + `Value`, `Readback`, `Transport`, `TransportLaws`, `CompLaws`, + `Glue`, `System`, `Soundness`) gets new arms. +- All existing axioms keep their statements; new ones added for the + new constructors. The total axiom count grows. No old axiom is + removed. +- The `CTerm`/`CType` constructor *tags* will shift if we insert new + constructors mid-list. Rust `tags.rs` and any tag-dispatching Rust + module pin tags via the Lean order — those need synchronised + updates. We pin REL1 tag layout in §6 of this doc. +- The Rust ABI version bumps from `1` to `2` (REL1). + +--- + +## 1. The problem + +Paideia's K7 (`BootstrapGradient`) is ideologically a literal cubical +`Path` between two `MasteryProvenance` values. `MasteryProvenance` is +a `Trace KnowledgeNode` — a list of records. Encoding it as a CTerm +of a `Path`-typed CType requires a `CType` for "list of `KnowledgeNode` +serialisations." The engine currently has no inductive types — only +`univ | pi | path | sigma | glue`. So `toCTerm : MasteryProvenance → +CTerm` is undefinable. + +The same shape recurs for every downstream consumer that wants to +embed Lean-inductive data into the cubical universe: + +- `Color/Space.lean` (modular color spaces) — was sketched as a HIT. +- Future cell-graph rendering inputs. +- Cubical Path-equality on `Bool`, `Nat`, `List` — needed for any + serious bridge to discrete-math reasoning. + +REL1 unblocks all of these in one move. + +--- + +## 2. Schema model — the data + +### 2.1 Argument shape + +```lean +inductive CTypeArg where + /-- Non-recursive arg of a fixed CType (may reference schema params + via `.param i` inside `A`). Examples: `cons : A → List A → List A` + has its first arg as `.type (CType.ind ListSchema [.param 0])` + shadowed via the param mechanism — see §2.4. -/ + | type (A : CType) + /-- The `i`th schema parameter (zero-indexed against `numParams`). -/ + | param (i : Nat) + /-- Recursive reference to the inductive being defined. Distinct + from `.type (CType.ind …)` because schemas are open-recursive + until they're inhabited — `.self` lets us state the schema + without a fixpoint operator. -/ + | self + /-- Dimension binder. Used in path constructors. When the ctor is + applied with a concrete `DimExpr`, the elimination rule consults + the boundary system to decide whether to produce the raw value + or fire a clause. -/ + | dim + deriving Repr, BEq +``` + +### 2.2 Constructor specification + +```lean +structure CtorSpec where + /-- Constructor name. Must be unique within a schema. -/ + name : String + /-- Argument list, in order. The boundary system (below) may refer + to args by index; ctor application supplies one CTerm per arg + in this order. -/ + args : List CTypeArg + /-- Boundary partial-element system. Empty list ≡ point ctor. + Non-empty list ≡ path ctor: each clause says "on this face of + the dim args, this ctor reduces to this value (a CTerm in scope + where the args are bound)." + + Coherence obligations on the clauses (enforced at + schema-validation time, not by the type of `boundary`): + + 1. Every face mentioned in the clause refers only to `.dim` + args of this ctor. + 2. Clause faces are pairwise compatible — overlapping faces + agree on the overlap. + 3. The collection of clause faces, taken as a join, equals the + outer boundary of the cube formed by the dim args (i.e. for + `k` dim args there are `2k` faces and every dimension's + endpoints must be specified, possibly via `.top`-faced + clauses if the boundary is constant). + -/ + boundary : List (FaceFormula × CTerm) + deriving Repr +``` + +### 2.3 Schema + +```lean +structure CTypeSchema where + name : String + numParams : Nat + ctors : List CtorSpec + deriving Repr +``` + +Equality on schemas is *structural by schema name + numParams + ctor +list*. The engine doesn't intern schemas; two schemas with the same +name in different modules are distinct values. + +### 2.4 Embedding into `CType` / `CTerm` + +```lean +inductive CType where + | univ + | pi (A B : CType) + | path (A : CType) (a b : CTerm) + | sigma (A B : CType) + | glue (φ : FaceFormula) (T : CType) + (f fInv sec ret coh : CTerm) (A : CType) + /-- NEW: an instance of a schema-defined inductive type at given + parameters. `params.length = S.numParams` is a typing-side + condition. -/ + | ind (S : CTypeSchema) (params : List CType) + +inductive CTerm where + | var, lam, app, plam, papp, transp, comp, compN + | glueIn, unglue + | pair, fst, snd + /-- NEW: constructor application. `ctorName` selects the clause + from `S.ctors`; `params` matches the schema parameters; `args` + supplies one CTerm per `CtorSpec.args` entry, with the + same arity ordering. -/ + | ctor (S : CTypeSchema) (ctorName : String) + (params : List CType) (args : List CTerm) + /-- NEW: induction principle / eliminator. `motive` is a CTerm + defining `λ x : .ind S params. Type` — i.e. a function whose + body is a CType expression with the bound name in scope. + `branches` lists `(ctorName, body)` pairs in *schema-declaration + order*; each branch's `body` is a CTerm taking the ctor's args + *and one extra arg per recursive `.self` arg* (the recursive + hypothesis, i.e. the result of the eliminator on the recursive + sub-value). `target` is the inductive-typed term being + eliminated. -/ + | indElim (S : CTypeSchema) (params : List CType) + (motive : CTerm) + (branches : List (String × CTerm)) + (target : CTerm) +``` + +A constructor's `args` carries its *full* arg list, including dim +args. When typing `.ctor S "loop" params [d]`, we know from `S.ctors` +that `loop` has `[.dim]`, so `d` must be a `CTerm` interpreted as a +`DimExpr` (we lift via `CTerm.var`-of-the-dim's name; or via a new +`CTerm.dimExpr (r : DimExpr) : CTerm` constructor — see §2.5). + +### 2.5 Dim args at the term level + +Path-ctor application crosses the term/dim boundary. Two options: + +**Option A — borrow `.var x`:** The dim-arg position in +`CTerm.ctor`'s `args` carries a `CTerm.var "i"` whose name happens to +be a `DimVar` name. Subst, eval, and dispatch all special-case "this +position is a dim arg" and read the name as a `DimVar`, looking it up +in a dim environment that the cubical evaluator maintains in parallel. + +Pros: no new CTerm constructor. Cons: punny & ambiguous; substituting +a non-var DimExpr (like `.meet i j`) is impossible without re-encoding. + +**Option B — new `CTerm.dimExpr (r : DimExpr) : CTerm`:** A first- +class CTerm carrying a dim expression. Only legal in dim-arg +positions; ill-typed elsewhere. + +Pros: fully general; `meet`/`join`/`inv` of dim args are expressible. +Cons: one more CTerm constructor; one more substitution arm; one more +eval / readback / typing rule. + +**Decision: Option B.** The user mandate is "no shortcuts." Path +constructors may want `.meet i j`-shaped boundary applications later +(e.g., for higher cubes), so we pay the constructor cost now. REL1 +ships `CTerm.dimExpr`. + +--- + +## 3. Worked examples + +### 3.1 `Nat` + +``` +schema Nat: + numParams = 0 + ctors: + .point "zero" [] + .point "succ" [.self] +``` + +``` +CType: .ind NatSchema [] +zero ::= .ctor NatSchema "zero" [] [] +succ n::= .ctor NatSchema "succ" [] [n] +``` + +### 3.2 `List A` + +``` +schema List: + numParams = 1 + ctors: + .point "nil" [] + .point "cons" [.param 0, .self] +``` + +``` +CType: .ind ListSchema [A] +nil ::= .ctor ListSchema "nil" [A] [] +cons x::= λxs. .ctor ListSchema "cons" [A] [x, xs] +``` + +### 3.3 `Bool` + +``` +schema Bool: + numParams = 0 + ctors: + .point "false" [] + .point "true" [] +``` + +### 3.4 `S¹` + +``` +schema S¹: + numParams = 0 + ctors: + .point "base" [] + .path "loop" [.dim "i"] -- one dim binder, named for boundary refs + boundary: + [(.eq0 i, base()), (.eq1 i, base())] +``` + +Note: `.dim` carries no name in `CTypeArg` — boundary clauses +reference dim args positionally (the *kth* `.dim` in `args` becomes +`DimVar.mk "$d_k"` at typing time). + +### 3.5 Propositional truncation `‖A‖₋₁` + +``` +schema PropTrunc: + numParams = 1 -- A + ctors: + .point "in" [.param 0] + .path "squash" [.self, .self, .dim] + boundary: + [(.eq0 d, /-arg 0-/), (.eq1 d, /-arg 1-/)] +``` + +(Boundary clause bodies use a positional `argRef`-encoding inside +their CTerm — see §4.) + +### 3.6 Suspension `Σ A` + +``` +schema Susp: + numParams = 1 + ctors: + .point "north" [] + .point "south" [] + .path "merid" [.param 0, .dim] + boundary: + [(.eq0 d, north()), (.eq1 d, south())] +``` + +--- + +## 4. Boundary system semantics + +The `boundary : List (FaceFormula × CTerm)` field has body CTerms in a +specific scope: the ctor's args are *all* in scope, addressed by +`CTerm.var "$arg_k"` where `k` is the arg index. The face formulae +range over the dim args, addressed by `DimVar.mk "$d_k"` where `k` is +the *dim*-arg index (counted only among `.dim` args). + +When `eval` encounters `.ctor S c params args`: + +1. Resolve the ctor spec: `cs := S.ctors.find name == c`. +2. Build a dim-evaluation environment from the dim args of `args`: + `dimEnv := λ d. eval-as-DimExpr (args.nth idxOfDim_d)`. +3. Evaluate each boundary clause's face: `φ.eval dimEnv`. +4. If any clause's face evaluates to `true` (canonical), substitute + the clause body (with arg references resolved) and evaluate that + instead. +5. Otherwise, the ctor application is canonical — produce + `CVal.vctor`. + +A path ctor with all-`.bot` boundary faces is canonical at every +generic dim — it acts like a free higher-dimensional generator. + +--- + +## 5. Eliminator (`indElim`) + +``` +indElim S params motive [(c₁, b₁), (c₂, b₂), …] target : CTerm +``` + +Typing rule sketch: + +1. `target : .ind S params`. +2. `motive : .pi (.ind S params) .univ` (depending on whether we + model the motive as a function or a closed `CType`-valued term — + REL1 ships the `pi`-valued form). +3. For each ctor `cᵢ`: + - The branch `bᵢ` has type + `args.foldr (λa rest. matchArg a rest) (.app motive (rebuilt-ctor))` + - `matchArg`: + - `.type A` → `.pi A rest` + - `.param j` → `.pi (params.nth j) rest` + - `.self` → `.pi (.ind S params) (.pi (.app motive bvar) rest)` + — i.e. take the recursive arg *and* the recursive hypothesis. + - `.dim` → `.path … …` — the dim is universally quantified + over the interval (modelled as a closed plam). +4. For path ctors, the branch must satisfy boundary coherence: at + each `(φ, body)` of the ctor's boundary, the branch evaluated at + the corresponding face equals the appropriate substitution into + the corresponding ctor (recursively eliminated). This is a + typing-level side condition mirroring `.comp`'s compatibility + condition. + +Reduction rule (β): + +``` +indElim S params M [(c₁,b₁), …] (ctor S cᵢ params [a₁,…,aₘ]) + ⟶ bᵢ a₁ … aₘ ih₁ … ihₖ +``` + +where `ihⱼ` is the `indElim`-result of each `.self`-typed argument. + +--- + +## 6. Constructor tag layout (REL1 freeze) + +Lean's `inductive` assigns tags in declaration order. Rust dispatch +relies on this order. REL1 freeze: + +**`CType` tags (REL1):** + +| Tag | Constructor | Notes | +|-----|-------------|-------| +| 0 | `.univ` | unchanged from REL0 | +| 1 | `.pi` | unchanged | +| 2 | `.path` | unchanged | +| 3 | `.sigma` | unchanged | +| 4 | `.glue` | unchanged | +| 5 | `.ind` | **NEW** | + +**`CTerm` tags (REL1):** + +| Tag | Constructor | +|-----|-------------| +| 0 | `.var` | +| 1 | `.lam` | +| 2 | `.app` | +| 3 | `.plam` | +| 4 | `.papp` | +| 5 | `.transp` | +| 6 | `.comp` | +| 7 | `.compN` | +| 8 | `.glueIn` | +| 9 | `.unglue` | +| 10 | `.pair` | +| 11 | `.fst` | +| 12 | `.snd` | +| 13 | `.dimExpr` | **NEW** | +| 14 | `.ctor` | **NEW** | +| 15 | `.indElim` | **NEW** | + +**`CVal` tags (REL1):** + +| Tag | Constructor | +|-----|-------------| +| 0 | `.vlam` | +| 1 | `.vplam` | +| 2 | `.vneu` | +| 3 | `.vTranspFun` | +| 4 | `.vHCompFun` | +| 5 | `.vTubeApp` | +| 6 | `.vCompFun` | +| 7 | `.vPathTransp` | +| 8 | `.vpair` | +| 9 | `.vctor` | **NEW** — fully-applied schema constructor | + +**`CNeu` tags (REL1):** + +| Tag | Constructor | +|-----|-------------| +| 0 | `.nvar` | +| 1 | `.napp` | +| 2 | `.npapp` | +| 3 | `.ntransp` | +| 4 | `.ncomp` | +| 5 | `.nhcomp` | +| 6 | `.ncompN` | +| 7 | `.nglueIn` | +| 8 | `.nunglue` | +| 9 | `.nfst` | +| 10 | `.nsnd` | +| 11 | `.nIndElim` | **NEW** — stuck eliminator | + +**Rust ABI version bump:** `TOPOLEI_FFI_ABI_VERSION 1 → 2`. + +--- + +## 7. Reductions (axiom catalogue) + +### 7.1 `eval` arms + +- `eval_ctor` — `eval env (.ctor S c params args) = .vctor S c params (args.map (eval env))` for point ctors. +- `eval_ctor_path_face_fires` — for path ctors, when one of the + boundary clauses' face evaluates to `true` under the dim-env from + the supplied args, eval substitutes that clause body and + re-evaluates. +- `eval_indElim_ctor` — β-reduction of the eliminator on a + fully-applied constructor. +- `eval_indElim_stuck` — produces `.vneu (.nIndElim …)` when target + is neutral. +- `eval_dimExpr` — `eval env (.dimExpr r) = .vdimExpr r` (or routes + through a `vdim` neutral; design pending — placeholder pinned at + REL1 implementation time). + +### 7.2 Transport + +- `eval_transp_ind_const` — when every parameter is dim-absent from + the binder, transport over `.ind S params` is identity (T2). +- `eval_transp_ind_pointwise` — transport over a varying-parameter + inductive applied to a `.vctor` distributes pointwise: each + non-recursive arg is transported via its CType's transport rule; + each `.self` arg is transported via the same outer-`.ind` + transport recursively. +- `eval_transp_ind_path_ctor` — for path ctors, transport must + respect the boundary system; CCHM gives the explicit formula via + `comp`-shaped fillers. +- `eval_transp_ind_stuck` — `.vneu (.ntransp …)` for non-canonical + targets. + +### 7.3 Composition + +- `eval_comp_ind_const`, `eval_comp_ind_pointwise`, + `eval_comp_ind_path_ctor`, `eval_comp_ind_stuck` — analogous to + `pi` rules in the existing `CompLaws.lean`. + +### 7.4 Readback + +- `readback_vctor` — `vctor S c params vargs ⟶ .ctor S c params (vargs.map readback)` +- `readbackNeu_nIndElim` — straightforward. + +--- + +## 8. FFI surface (REL1) + +Add to `native/cubical/include/topolei_cubical.h`: + +```c +lean_obj_res topolei_cubical_vIndElim( + b_lean_obj_arg env, b_lean_obj_arg S, b_lean_obj_arg params, + b_lean_obj_arg motive, b_lean_obj_arg branches, + b_lean_obj_arg target); + +lean_obj_res topolei_cubical_vCtor( + b_lean_obj_arg S, b_lean_obj_arg name, + b_lean_obj_arg params, b_lean_obj_arg args); +``` + +`eval` / `readback` / `subst` / `dim_absent` — extend tag-dispatch +arms in Rust to cover `CTerm.{dimExpr, ctor, indElim}`, +`CType.ind`, `CVal.vctor`, `CNeu.nIndElim`. + +Substitution of `.var`-named dim args inside `CTerm.dimExpr` follows +the same path as `DimExpr.subst` already does — Rust `subst.rs` gains +a single arm. + +--- + +## 9. Migration notes (downstream consumers) + +### 9.1 `topolei` (sibling repo) — concrete impact + +Surveyed against `topolei` HEAD (2026-04-30). Six files import +`CubicalTransport.*` and pattern-match on engine types; the breakage +is well-bounded — every match is structural recursion that mirrors +the existing `compN`/`pair`/`unglue` shape, so new constructors slot +in cleanly. + +| File | Match shape | New arms required | +|------|-------------|-------------------| +| `Topolei/Cubical/DecEq.lean` | exhaustive `CTerm.beq` (13 arms), `CType.beq` (5 arms), reflexivity proofs | +1 `CType` arm (`.ind`); +3 `CTerm` arms (`.dimExpr`, `.ctor`, `.indElim`) | +| `Topolei/Cubical/Trace.lean` | exhaustive `CTerm.traceOf` recursing into every sub-CTerm | +3 `CTerm` arms; structural — recurse via `Trace.union` over `args` / `branches` / `target` | +| `Topolei/Cubical/TraceAt.lean` | exhaustive `CTerm.traceOfAt`; **13 per-constructor `subTrace_*` lifting lemmas** | +3 arms in `traceOfAt`; +3 new lifting lemmas (`subTrace_dimExpr`, `subTrace_ctor`, `subTrace_indElim`) | +| `Topolei/Cubical/FluxR.lean` | exhaustive `CTerm.fluxAtAcc` (Float-weighted face propagation) | +3 arms; flux weight = `min` over sub-CTerms (same pattern as `compN`) | +| `Topolei/EML/Path.lean` | none on `CType`/`CTerm` — uses `DimLine` as a black box | none | +| `Topolei/EML/Cubical.lean` | partial `CTerm.evalEML` with `_ => 0.0` fallback (intentional) | none — fallback handles new shapes | + +**Schema/CtorSpec/CTypeArg/dimExpr design choice — why it fits topolei:** +the new `CTerm.{dimExpr, ctor, indElim}` constructors all have either +no sub-CTerms (`dimExpr`) or a flat `List CTerm` of sub-terms (`args`, +`branches.map .2`, `motive`, `target`). Topolei's recursors all +already handle the "list of sub-CTerms" shape (see `compN`'s clauses +arm in `Trace.lean:107`). No new recursion machinery is needed — the +new arms are mechanical. + +**`CTypeSchema` is opaque to topolei.** The schema is part of the +mutual inductive block at the engine level, but topolei never +pattern-matches on `CTypeSchema` / `CtorSpec` / `CTypeArg` directly — +it only sees them as opaque payloads inside `CType.ind` / `CTerm.ctor` / +`CTerm.indElim`. Schema-internal CTerms (boundary clause bodies) +are static schema-level data, not part of any user term's trace. + +**Migration plan for topolei (post-engine REL1 merge):** + +1. Extend `DecEq.lean`: add ind-arm to `CType.beq`; add three arms to + `CTerm.beq` plus refl proofs. Decision: equality on `CTypeSchema` + inside `CType.ind` reduces to schema *name* equality plus `params` + equality (REL1 does not intern schemas; structural equality on + the full schema struct is provided as a separate decision + procedure — see §11.2). +2. Extend `Trace.lean`'s `traceOf` and the helper clause recursor. +3. Extend `TraceAt.lean`'s `traceOfAt`, `traceOfAt.clauses`, plus + add the three new lifting lemmas matching the existing 13. +4. Extend `FluxR.lean`'s `fluxAtAcc` (and its clause helper). +5. `Path.lean`, `EML/Cubical.lean` — no changes needed. + +Estimated topolei migration: ~150–250 lines across the four files, +mostly mechanical recursion arms. + +### 9.2 `paideia` and other downstream + +Paideia is the *driver* of this refactor — its K7 work depends on it. +Migration sequence in §9.3 of the original issue body. Other +downstream consumers (any project depending on `topolei` rather than +the engine directly) get the breakage indirectly through topolei's +`Trace`/`TraceAt`/`FluxR` API surface, which is preserved by name +(only the new arms are added). + +### 9.3 Rust kernel + +`native/cubical/src/{tags.rs, value.rs, eval.rs, readback.rs, +subst.rs, dim_absent.rs}` all switch on Lean constructor tags. REL1 +freezes the new tag layout in §6 above; Rust modules update in +lockstep. ABI version bumps to `2`. + +### 9.2 `paideia` + +- `Paideia/Foundation/K7Cubical.lean` retires `MathPath` in favour of + `CTerm`-typed values of `Path (.ind ListSchema [KNodeCType])`. +- New module `Paideia/Foundation/MasteryEncoding.lean` defines + `KnowledgeNode.toCTerm`, `MasteryProvenance.toCTerm` (using + `ListSchema`), and the inverse parser. +- K7's external API (`init`, `step`, `lift`) keeps its types; only + the under-the-hood representation moves to engine-grounded paths. + +--- + +## 10. Test plan + +### 10.1 Plain inductives + +- `nat_zero_succ_eval` — eval `succ (succ zero)` to `vctor … "succ" [vctor … "succ" [vctor … "zero" []]]`. +- `list_cons_nil_eval` — same shape, parameterised. +- `nat_indElim_plus` — define `plus : Nat → Nat → Nat` via indElim; + eval `plus 2 3 = 5` (engine-side). +- `transp_const_list_id` — transport over a constant `List Nat` line + is identity. + +### 10.2 HITs + +- `s1_loop_endpoints` — `loop @ 0 = base`, `loop @ 1 = base`. +- `prop_trunc_squash` — any two `‖A‖₋₁` values are connected by a path. +- `susp_merid_endpoints` — `merid a @ 0 = north`, `merid a @ 1 = south`. +- `transp_s1_const` — transport over a constant S¹ line is identity. + +### 10.3 Cross-cutting + +- Property tests: schemas with N constructors and M dim args, random + ctor application; check that boundary firing is consistent with + manual reduction. +- Differential fuzz against Rust impl: post-Phase-D regression suite. + +--- + +## 11. Open questions (REL1 implementation) + +1. **Schema interning.** We don't intern schemas in REL1 (every + `.ind` carries the schema by value). This means schemas are + structurally compared. If schemas grow large, switch to a global + registry keyed by `name`. Defer until profiling justifies. +2. **Equality on schemas.** Lean's `deriving BEq`/`DecidableEq` + over `CTypeSchema` is non-trivial because `CtorSpec.boundary` + contains `CTerm`s, which mutually recurse with `CType`. We + deliberately don't derive `BEq` — equality is structural per + the inductive definition; any `BEq` instance is provided by a + bespoke decision procedure (REL1.1, post-merge). +3. **Soundness chapter.** The transport-over-HIT chapter + (cells-spec §14, "HIT transport") becomes a real deliverable in + REL1 alongside the new axioms. Statement and proof obligations + listed in §11 of `Soundness.lean` after the refactor. + +--- + +*End of INDUCTIVE_TYPES.md. This document is the contract between +the engine refactor and downstream consumers. Update on every API +shape change before the change lands.*