cubical-transport-hott-lean4/docs/QUESTIONS.md

QUESTIONS.md — The Universal Question Form

Drafted 2026-04-30 on Dev_REL2. Captures the design philosophy behind the project's question-as-data discipline — first surfaced mid-REL2 as the substrate underlying both Bridge.lean and the planned Dev_Algebra macro layer. Companion to REL2_PLAN.md (implementation) and EULERIAN.md (poetic register).

---

0. The motivation, in one paragraph

In the discrete-math world, a clean Lean 4 file like differential_equations.lean first defines a vocabulary of question-shapes (IsExact, IsBernoulli, IsHomogeneous, …) as predicates over the data of an ODE, and then states each problem as a theorem whose type encodes the question. Solutions follow. The crucial move is that questions are first-class types: you can compare them, equivalence-class them, prove implications between them, even before you answer any.

The same discipline applies, with surprising force, to cubical type theory — because cubical type theory has a single canonical universal question form, and we already have the engine that answers every instance of it.

---

1. The universal question form

Given a type-line A(i) along a dimension binder i, a face formula φ, a partial element u : A defined on φ, and a base t : A(0), find a total element v : A(1) agreeing with u on φ and with t at i = 0.

This is the partial-element-filler problem (CCHM §3, §5). Its universal answer is the cubical comp operator:

comp i A φ u t : A(1)

Every cubical operation we have is a specialisation of this universal question:

Operation	Specialisation of comp
transp i A φ t	comp i A φ t t — base equals partial element (no side condition)
hcomp A φ u t	comp i A φ u t with A constant in i
compN	comp with a multi-clause partial element
Path β / η	comp instantiated at Path types with appropriate boundaries
Glue β / η	comp instantiated at Glue types with the equivalence's filler
Univalence	comp over uaLine evaluating an equivalence at an endpoint

Transport is the degenerate question: "extend t along A(i) with no side constraints." All others add structure (a non-trivial partial element on a non-trivial face) without changing the question shape. The question is universal; only its parameters vary.

---

2. Reifying the question as data

The shape of comp becomes a Lean record:

namespace Question

structure CompQ where
  env    : CEnv
  binder : DimVar
  body   : CType            -- A(i) — the type-line
  φ      : FaceFormula      -- where u lives
  u      : CTerm            -- partial element on φ
  t      : CTerm            -- base at i=0

/-- "Asking" a question runs the engine. -/
def CompQ.ask (q : CompQ) : CVal :=
  vCompAtTerm q.env q.binder q.body q.φ q.u q.t

/-- Two questions are equivalent if their answers coincide. -/
def CompQ.Equiv (q₁ q₂ : CompQ) : Prop :=
  q₁.ask = q₂.ask

/-- Subsumption: q₁ ≤ q₂ when q₂'s answer specialises to q₁'s. -/
def CompQ.Refines (q₁ q₂ : CompQ) : Prop := …

end Question

Transport is a derived shape:

def TranspQ.toCompQ (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm) : CompQ :=
  { env := env, binder := i, body := A, φ := φ, u := t, t := t }

Equivalences, derivations, and witnesses become morphisms in the implicit category of CompQ values.

---

3. Classifiers — the meta-vocabulary of question shapes

Mirroring ODE.IsExact, ODE.IsBernoulli, …, every cubical question admits classifying predicates that pin its specific shape:

namespace Question

/-- The line is constant in its binder — transport / comp is identity
    on the body. -/
def IsConstLine (q : CompQ) : Prop :=
  q.body.dimAbsent q.binder = true

/-- The face is the full face — partial element covers the whole
    space. -/
def IsFullFace (q : CompQ) : Prop := q.φ = .top

/-- The face is the empty face — only the base contributes. -/
def IsEmptyFace (q : CompQ) : Prop := q.φ = .bot

/-- The base equals the partial element — this is a transport, not
    a heterogeneous comp. -/
def IsTransport (q : CompQ) : Prop := q.u = q.t

/-- The line is a Path type — Path-specific reductions apply. -/
def IsPathLine (q : CompQ) : Prop :=
  ∃ A₀ a b, q.body = .path A₀ a b

/-- The line is a Glue type — Glue-specific reductions apply. -/
def IsGlueLine (q : CompQ) : Prop :=
  ∃ ψ T f fInv s r c A,
    q.body = .glue ψ T f fInv s r c A

/-- The line is a Π type — CCHM Π reductions apply. -/
def IsPiLine (q : CompQ) : Prop :=
  ∃ domA codA, q.body = .pi domA codA

/-- The line is a schema-defined inductive — REL1 reductions apply. -/
def IsIndLine (q : CompQ) : Prop :=
  ∃ S params, q.body = .ind S params

/-- The line is the cubical interval — REL2 transport-on-𝕀 is
    identity. -/
def IsIntervalLine (q : CompQ) : Prop :=
  q.body = .interval

end Question

Every existing reduction axiom in the codebase becomes a theorem about classifier-conditioned question equivalence:

-- eval_transp_top, today an axiom-side lemma:
-- eval env (.transp i A .top t) = eval env t
--
-- becomes the question-equivalence theorem:
theorem CompQ.full_face_is_identity
    (q : CompQ) (h : IsFullFace q) :
    q.Equiv (CompQ.identity q.env q.t)

-- eval_transp_const:
theorem CompQ.const_line_is_identity
    (q : CompQ) (h₁ : IsConstLine q) (h₂ : IsTransport q) :
    q.Equiv (CompQ.identity q.env q.t)

-- eval_transp_pi (the full CCHM Π rule):
theorem CompQ.pi_line_is_vTranspFun
    (q : CompQ) (h : IsPiLine q) (hT : IsTransport q)
    (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) :
    q.Equiv (CompQ.viaTranspFun …)

Each theorem is one move in the question algebra: applying a classifier rewrites the question to a simpler one, in a way that runs through q.Equiv and so chains under composition.

---

4. Three levels of commitment

The question discipline supports three escalating levels:

4.1 Level 1 — Structural reification only ✅ LANDED 2026-05-01

Define CompQ, ask, Equiv, classifiers. Restate existing axioms / theorems as classifier-conditioned equivalences. Existing runtime / soundness behaviour unchanged.

Status: landed in CubicalTransport/Question.lean on Dev_REL2 as commit 6adbce0 (2026-05-01). CompQ + 11 classifiers + 5 ask_of_* theorems for the eval_comp_* family.

Benefit: a uniform vocabulary; new theorems are naturally stated in question form; old theorems become derived corollaries.

4.2 Level 2 — Routing through questions ✅ LANDED 2026-05-01

Every axiom and theorem in Eval / TransportLaws / CompLaws / Glue re-stated in question shape. A simp-set rewrites question equivalences. Call sites continue to work via q.ask = … lemmas.

Status: landed as commit d6af78a (2026-05-01). TranspQ + HCompQ + CompNQ sister questions; transport / hcomp / compN axioms restated as classifier-conditioned Equiv theorems with @[simp] tags; bridge TranspQ.toCompQ_ask_eq_ask_full_face reconciles transport-as-itself with transport-as-degenerate-comp.

Benefit: question algebra — compose, decompose, refine mechanically. Refactors (rename a classifier, factor a question, merge two questions into a join) become text-level operations that preserve correctness.

4.3 Level 3 — Question-driven proofs ✅ PARTIAL (light) 2026-05-01

Proofs are question reductions: "this CompQ reduces to that CompQ, which is identity by IsConstLine." A cubical_simp tactic knows the reduction graph and finds reduction chains automatically.

Status:

• ✅ Light form (cubical_simp macro) — landed as commit d6af78a (2026-05-01). A macro tactic expanding to a simp only call pre-loaded with every classifier definition + every @[simp]-tagged ask_of_* lemma. Concrete-shape questions collapse automatically; arbitrary extra simp lemmas can be passed via cubical_simp [extra_args].
• ✅ Autodiscovery search (cubical_search tactic) — landed in CubicalTransport/Algebra/Methodology.lean per ALGEBRA_PLAN.md Phase D' as part of the metacoding stack.
• ⏳ Full graph-walking form — the version that walks the classifier-equivalence graph step-by-step with structured failure reports per §4.4 below. Depends on @[metaPath] declarations (REL2.6+).

Benefit: proofs become navigable graphs of classifier applications; the engine essentially proves cubical-core theorems automatically.

---

5. The connection to comp lifted to the meta-level

The deepest insight: the same question-form algebra also describes the macro layer that organises the codebase itself. See ALGEBRA_PLAN.md for the full plan; the headline:

A meta-restructuring operation has signature

restructure
  (i        : MetaPosition)         -- where in the source
  (Context  : MetaCType)            -- what kind of artifact
  (φ        : MetaClassifier)       -- when this restructuring applies
  (witness  : MetaArtifact)         -- new content valid on φ
  (fallback : MetaArtifact)         -- existing content off-φ

— exactly the same five-field shape as comp i A φ u t, with each field promoted from "cubical CTerm" to "structural Lean artifact." The macro layer is comp reflecting itself one level up.

Concretely, the autodiscovery tactic cubical_search is restructure whose (witness, fallback) is computed by search over a methodology library, with new methodologies derived automatically from old ones via transport along structural Paths in the codebase — transp lifted to the methodology level.

The whole design discipline collapses to: one universal question form, used at three levels (cubical / question / meta), each level the reflection of the level below.

---

6. Why this matters for downstream consumers

6.1 Internal: cubical-core proofs

Every existing axiom + theorem in the cubical engine (eval_transp_*, eval_comp_*, the 9 Glue-transport face-disjoint variants, transp_ua, glue_beta, …) is a classifier-conditioned question-equivalence. Pulling them through CompQ.Equiv makes the dependency graph visible: which classifiers chain to which others, which questions are foundational vs. derived, where the axiom-discharge load actually concentrates.

6.2 External: paideia / topolei

Bridge.lean already provides the Eq ↔ Path ferry between Lean's Eq world and the cubical Path world. In the question-form discipline, Bridge's instances become classifier libraries — "a question whose body is the Bool-schema-CType is answerable via this discrete-equality chain." Future paideia / topolei / cells-spec consumers register their own classifier libraries; the core engine doesn't grow new code.

6.3 Tooling: code actions, tactics, search

A code action in the editor (REL2.5+ Dev_Algebra) operates on CompQ values: "factor this question into two simpler ones," "rename this classifier across all dependents," "transport this methodology along that path." Every action is a typed operation in the question algebra, and the tooling never has to special-case arbitrary tactic scripts.

---

7. Open questions (logged here, not blocking)

1. Schema for question-graph storage. In-memory (computed each LSP session) vs. persisted as Lean attributes (@[question Foo], @[classifier IsConstLine]) — REL2.5 design decision.
2. Higher questions. Equivalences between classifier-equivalences (paths between paths) — natural to want; probably out of scope until cells-spec §8 (n-cells).
3. Question algebra completeness. Is every cubical theorem provable as a chain of classifier-conditioned equivalences? We conjecture yes for the core axiom set; verifying is part of Level 3 work.
4. Decide-checkable classifiers. Most classifiers are syntactic (q.φ = .top, q.body.dimAbsent q.binder = true) and thus Decidable. Some (IsPathLine, etc.) involve existentials; need explicit DecidableEq / inversion lemmas. Tracked in REL2.5 OQ list.

---

End of QUESTIONS.md. Companion to REL2_PLAN.md (Phase plan), ALGEBRA_PLAN.md (macro / dev-branch design), and EULERIAN.md (poetic record).