cubical-transport-hott-lean4/CubicalTransport/Question.lean

/-
  CubicalTransport.Question — The universal question form
  =======================================================
  Implements `docs/QUESTIONS.md` Levels 1 + 1.5 + 2.

  The CCHM partial-element-filler problem `comp i A φ u t` is *the*
  universal cubical question.  This module reifies that question as
  a Lean record `CompQ`, defines `ask` (run the engine), `Equiv`
  (answers coincide), and a vocabulary of classifying predicates
  that pin specific question shapes (`IsConstLine`, `IsFullFace`,
  `IsPathLine`, …).

  Four reified question shapes:

    · `CompQ`   — heterogeneous comp on `(env, binder, body, φ, u, t)`,
                  the universal CCHM partial-element-filler.
    · `TranspQ` — transport `(env, binder, body, φ, t)`; engine-distinct
                  from `CompQ.ofTransp` (the latter routes through
                  `eval (.comp ...)` whose full-face arm substitutes
                  `t.substDim binder .one` instead of `eval env t`).
    · `HCompQ`  — homogeneous comp on `(body, φ, tube, base : CVal)`;
                  delegates to `vHCompValue`.
    · `CompNQ`  — multi-clause heterogeneous comp on
                  `(env, binder, body, clauses : List (FaceFormula × CTerm), t)`;
                  delegates to `vCompNAtTerm`.

  Level commitments:

  - Level 1   — `CompQ` reified, classifiers, `eval_comp_*` axioms
                restated as classifier-conditioned `Equiv` theorems.
  - Level 1.5 — full DecidableEq on the AST (see `DecEq.lean`); every
                classifier `Decidable`.
  - Level 2   — `TranspQ`, `HCompQ`, `CompNQ` sister questions; every
                `eval_transp_*`, `vHCompValue_*`, `vCompNAtTerm_def`
                axiom restated as a question-form theorem with `@[simp]`
                tag, so `simp [question_simpSet]` routes through the
                classifier algebra automatically.
  - Level 3   — `cubical_simp` tactic (see `Cubical/Tactic.lean`).

  Companion: `docs/QUESTIONS.md` (philosophy), `docs/ALGEBRA_PLAN.md`
  (the macro layer this enables), `docs/EULERIAN.md` (poetic record).
-/

import CubicalTransport.TransportLaws
import CubicalTransport.CompLaws
import CubicalTransport.DecEq

-- The genuinely-equational classifier-conditioned theorems below are
-- tagged with `@[simp]` only.  Lean's standard `simp` finds them
-- automatically; no curated named-set is required.  Downstream
-- consumers can extend by tagging their own classifier-conditioned
-- theorems with `@[simp]` — same mechanism.
--
-- An earlier draft registered a custom `Question.simp` simp set via
-- `register_simp_attr`; that's strictly more curation than the
-- declarative-foundation principle calls for, so it was dropped.
-- Anyone wanting a project-local simp bundle can register one
-- downstream.

namespace Question

-- ── CompQ — the universal question, reified ─────────────────────────────────

/-- The CCHM partial-element-filler question, reified as data.

    Given a type-line `body` along binder `binder`, a face `φ`, a
    partial element `u` defined on `φ`, and a base `t` at `binder = 0`,
    `CompQ.ask` produces the engine's universal answer — a total
    element at `binder = 1` agreeing with `u` on `φ` and with `t` at
    `binder = 0`.

    Every cubical operation in the engine (`transp`, `hcomp`, `compN`,
    Path β/η, Glue β/η, univalence-transport) is a specialisation of
    this single shape.  See QUESTIONS.md §1 for the table. -/
structure CompQ where
  env    : CEnv
  binder : DimVar
  body   : CType
  φ      : FaceFormula
  u      : CTerm
  t      : CTerm

/-- "Asking" a question runs the engine on a `.comp` term.  Equivalent
    to `vCompAtTerm` by `Eval.lean`'s `.comp` arm of `eval`, but
    routed through `eval (.comp …)` so that the existing
    `eval_comp_*` axioms apply directly. -/
def CompQ.ask (q : CompQ) : CVal :=
  eval q.env (.comp q.binder q.body q.φ q.u q.t)

/-- Two questions are *equivalent* when their engine answers coincide.

    This is the coarsest useful relation: questions with different
    parameters can have the same answer.  It is reflexive, symmetric,
    and transitive (it's just `Eq` on `CVal`).  It is *not* the same
    as `q₁ = q₂` — two questions can share an answer without being
    syntactically identical. -/
def CompQ.Equiv (q₁ q₂ : CompQ) : Prop := q₁.ask = q₂.ask

@[refl] theorem CompQ.Equiv.refl (q : CompQ) : q.Equiv q := rfl

@[symm] theorem CompQ.Equiv.symm {q₁ q₂ : CompQ}
    (h : q₁.Equiv q₂) : q₂.Equiv q₁ := Eq.symm h

theorem CompQ.Equiv.trans {q₁ q₂ q₃ : CompQ}
    (h₁ : q₁.Equiv q₂) (h₂ : q₂.Equiv q₃) : q₁.Equiv q₃ :=
  Eq.trans h₁ h₂

/-- Smart constructor: every transport `transpⁱ A φ t` is the
    degenerate question `compⁱ A φ t t` (no side condition: the
    partial element equals the base).  See QUESTIONS.md §1, table
    row 1.

    The CompQ answer agrees with `eval env (.transp i A φ t)` when
    the base is constant in the line binder (the standard cubical
    typing premise); the engine's `vCompAtTerm` substitutes
    `t.substDim i .one` on the full-face case while `transp` runs
    `eval env t` directly.  See `CompQ.ask_of_transport_full_face`
    for the bridging lemma. -/
def CompQ.ofTransp (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm) : CompQ :=
  { env := env, binder := i, body := A, φ := φ, u := t, t := t }

-- ── Classifiers — the meta-vocabulary of question shapes ─────────────────────

/-- The line is constant in its binder — `comp` reduces to `hcomp`
    (or to identity, on a full face). -/
@[simp]
def IsConstLine (q : CompQ) : Prop :=
  q.body.dimAbsent q.binder = true

/-- The face is the full face — the partial element covers the whole
    space, so the answer is its `binder := 1` value. -/
@[simp]
def IsFullFace (q : CompQ) : Prop := q.φ = .top

/-- The face is the empty face — only the base contributes; the
    question reduces to plain transport. -/
@[simp]
def IsEmptyFace (q : CompQ) : Prop := q.φ = .bot

/-- The base equals the partial element — this is a transport
    expressed in `comp` form, not a heterogeneous composition. -/
@[simp]
def IsTransport (q : CompQ) : Prop := q.u = q.t

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

/-- The line is a Glue type — Glue-specific reductions apply. -/
@[simp]
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. -/
@[simp]
def IsPiLine (q : CompQ) : Prop :=
  ∃ domA codA, q.body = .pi domA codA

/-- The line is a Σ type — Σ reductions apply (REL2.x). -/
@[simp]
def IsSigmaLine (q : CompQ) : Prop :=
  ∃ A B, q.body = .sigma A B

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

/-- The line is the cubical interval — REL2 transport-on-𝕀 is
    identity (the interval is dim-absent in itself). -/
@[simp]
def IsIntervalLine (q : CompQ) : Prop :=
  q.body = .interval

/-- The line is the universe — universe-transport reductions apply
    (currently stuck; CCHM univalence-transport via `uaLine`). -/
@[simp]
def IsUnivLine (q : CompQ) : Prop :=
  q.body = .univ

/-- The body is non-Path, non-Glue, non-Π — useful for stating the
    `eval_comp_stuck` / `eval_transp_nonpath` discharge.  Combine with
    `¬IsConstLine` and `¬IsFullFace`/`¬IsEmptyFace` to pin the stuck
    case.  Lifted as `Prop` so it composes with the other classifiers. -/
def IsNonPathNonGlueNonPi (q : CompQ) : Prop :=
  (∀ A₀ a b, q.body ≠ .path A₀ a b) ∧
  (∀ φG T f fInv sec ret coh A, q.body ≠ .glue φG T f fInv sec ret coh A) ∧
  (∀ domA codA, q.body ≠ .pi domA codA)

-- ── Decidability for every classifier ───────────────────────────────────────
-- All classifiers are `Decidable`.  Syntactic ones (face / body-tag /
-- u=t equality) reduce directly to `DecidableEq` on existing types
-- (`FaceFormula`, `CType`, `CTerm` — the latter via the mutual
-- `decEq` block in `DecEq.lean`).  Existential body-shape classifiers
-- (`IsPathLine`, `IsGlueLine`, `IsPiLine`, `IsSigmaLine`, `IsIndLine`)
-- use `match h : q.body with` to inspect the head constructor and
-- reconstruct the existential witness.

instance (q : CompQ) : Decidable (IsConstLine q) :=
  inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true))

instance (q : CompQ) : Decidable (IsFullFace q) :=
  inferInstanceAs (Decidable (q.φ = .top))

instance (q : CompQ) : Decidable (IsEmptyFace q) :=
  inferInstanceAs (Decidable (q.φ = .bot))

instance (q : CompQ) : Decidable (IsTransport q) :=
  inferInstanceAs (Decidable (q.u = q.t))

instance (q : CompQ) : Decidable (IsIntervalLine q) :=
  inferInstanceAs (Decidable (q.body = .interval))

instance (q : CompQ) : Decidable (IsUnivLine q) :=
  inferInstanceAs (Decidable (q.body = .univ))

instance (q : CompQ) : Decidable (IsPathLine q) :=
  match h : q.body with
  | .path A₀ a b => isTrue ⟨A₀, a, b, h⟩
  | .univ | .pi _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsPiLine q) :=
  match h : q.body with
  | .pi domA codA => isTrue ⟨domA, codA, h⟩
  | .univ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsSigmaLine q) :=
  match h : q.body with
  | .sigma A B => isTrue ⟨A, B, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsGlueLine q) :=
  match h : q.body with
  | .glue ψ T f fInv s r c A => isTrue ⟨ψ, T, f, fInv, s, r, c, A, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, _, _, _, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsIndLine q) :=
  match h : q.body with
  | .ind S params => isTrue ⟨S, params, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

-- ── Restated axioms — classifier-conditioned question equivalence ─────────────
-- Level 1: each existing `eval_comp_*` axiom is restated as a
-- theorem about `CompQ.ask`.  These are derived (not new axioms);
-- they exist to give the question-form vocabulary first-class
-- access to the engine's reduction graph.
--
-- The pattern is always the same: classifiers on the LHS, an
-- equation about `q.ask` on the RHS.  Future Level 2 work will
-- chain these via `simp` on `CompQ.Equiv`.

namespace CompQ

/-- C1 in question form: full-face question's answer is the
    partial element substituted at `binder := 1`. -/
@[simp]
theorem ask_of_full_face (q : CompQ) (h : IsFullFace q) :
    q.ask = eval q.env (q.u.substDim q.binder .one) := by
  unfold ask
  rw [show q.φ = .top from h]
  exact eval_comp_top q.env q.binder q.body q.u q.t

/-- C2 in question form: empty-face question's answer is plain
    transport on the base. -/
@[simp]
theorem ask_of_empty_face (q : CompQ) (h : IsEmptyFace q) :
    q.ask = eval q.env (.transp q.binder q.body .bot q.t) := by
  unfold ask
  rw [show q.φ = .bot from h]
  exact eval_comp_bot q.env q.binder q.body q.u q.t

/-- Constant-line question: when the type doesn't vary along
    `binder`, heterogeneous comp reduces to `vHCompValue` (hcomp).
    Requires the face is neither full nor empty (those have their
    own theorems above). -/
@[simp]
theorem ask_of_const_line (q : CompQ)
    (hC : IsConstLine q)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q) :
    q.ask = vHCompValue q.body q.φ
      (eval q.env (.plam q.binder q.u)) (eval q.env q.t) := by
  unfold ask
  exact eval_comp_const q.env q.binder q.body q.φ q.u q.t hφ₁ hφ₂ hC

/-- Helper: the negation of `IsConstLine` rewrites to the `= false`
    form expected by `eval_comp_pi` / `eval_comp_stuck`. -/
private theorem dimAbsent_eq_false_of_not_isConstLine (q : CompQ)
    (h : ¬ IsConstLine q) :
    CType.dimAbsent q.binder q.body = false := by
  unfold IsConstLine at h
  match hb : CType.dimAbsent q.binder q.body with
  | true  => exact absurd hb h
  | false => rfl

/-- Π-line question: hetero comp on a Π type packages into a
    `vCompFun` closure that runs CCHM Π β at application time.
    Requires the face is non-trivial and the line genuinely varies. -/
theorem ask_of_pi_line (q : CompQ)
    (hP : IsPiLine q)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q)
    (hC : ¬ IsConstLine q) :
    ∃ domA codA, q.body = .pi domA codA ∧
      q.ask = .vCompFun q.env q.binder domA codA q.φ q.u q.t := by
  obtain ⟨domA, codA, hbody⟩ := hP
  refine ⟨domA, codA, hbody, ?_⟩
  unfold ask
  rw [hbody]
  apply eval_comp_pi q.env q.binder domA codA q.φ q.u q.t hφ₁ hφ₂
  have := dimAbsent_eq_false_of_not_isConstLine q hC
  rw [hbody] at this
  exact this

/-- Stuck question: face non-trivial, line genuinely varies, and
    type is neither Π nor any reducing shape — answer is a `ncomp`
    neutral.  Refinement of this for `IsIndLine`, `IsSigmaLine`,
    `IsIntervalLine`, etc., is Level 2 work. -/
theorem ask_of_stuck (q : CompQ)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q)
    (hC : ¬ IsConstLine q)
    (hP : ¬ IsPiLine q) :
    q.ask = .vneu (.ncomp q.binder q.body q.φ
      (eval q.env q.u) (eval q.env q.t)) := by
  unfold ask
  apply eval_comp_stuck q.env q.binder q.body q.φ q.u q.t hφ₁ hφ₂
  · exact dimAbsent_eq_false_of_not_isConstLine q hC
  · intro domA codA hb
    exact hP ⟨domA, codA, hb⟩

-- ── Transport-shaped corollary ──────────────────────────────────────────────

/-- Transport-shaped question (`u = t`) under a full face: when the
    base is constant in the line binder (the cubical typing premise),
    the answer is `eval env t`.  This is the bridge between
    `CompQ.ofTransp` and the legacy `eval_transp_top` axiom. -/
@[simp]
theorem ask_of_transport_full_face (q : CompQ)
    (hT : IsTransport q) (hφ : IsFullFace q)
    (hi : q.t.dimAbsent q.binder = true) :
    q.ask = eval q.env q.t := by
  rw [ask_of_full_face q hφ, show q.u = q.t from hT,
      CTerm.substDim_of_absent q.binder .one q.t hi]

end CompQ

-- ──────────────────────────────────────────────────────────────────────────
-- TranspQ — transport question
-- ──────────────────────────────────────────────────────────────────────────
--
-- Transport `transpⁱ A φ t` is *almost* a degenerate `comp` (the case
-- `compⁱ A φ t t`), but the engine treats them differently on the
-- full-face arm: `eval (.transp i A .top t) = eval env t` (T1), while
-- `vCompAtTerm env i A .top t t = eval env (t.substDim i .one)`
-- (which collapses to the same thing only when `t.dimAbsent i = true`).
--
-- For the question algebra to track the engine faithfully, we reify
-- transport as its own question shape with its own `ask` delegating
-- to `eval (.transp ...)`.  The bridge to `CompQ.ofTransp` is the
-- `TranspQ.toCompQ` direction with a typing-side base-dim-absent
-- premise (see `transp_eq_comp_when_base_const`).

/-- Transport question, reified as data.

    `(env, binder, body, φ, t)` represents the transport
    `transpⁱ body φ t` from `body(0)` to `body(1)` along the line
    `λ binder. body`, restricted by the face `φ`.  When `φ = .top`
    the transport is identity; when `body` is dim-absent in the
    binder, T2 makes it identity.  Path / Π / Glue / inductive
    bodies have specialised reductions captured below. -/
structure TranspQ where
  env    : CEnv
  binder : DimVar
  body   : CType
  φ      : FaceFormula
  t      : CTerm

/-- "Asking" a transport question runs the engine on `.transp`. -/
def TranspQ.ask (q : TranspQ) : CVal :=
  eval q.env (.transp q.binder q.body q.φ q.t)

/-- Two transport questions are equivalent when their answers agree. -/
def TranspQ.Equiv (q₁ q₂ : TranspQ) : Prop := q₁.ask = q₂.ask

@[refl] theorem TranspQ.Equiv.refl (q : TranspQ) : q.Equiv q := rfl
@[symm] theorem TranspQ.Equiv.symm {q₁ q₂ : TranspQ}
    (h : q₁.Equiv q₂) : q₂.Equiv q₁ := Eq.symm h
theorem TranspQ.Equiv.trans {q₁ q₂ q₃ : TranspQ}
    (h₁ : q₁.Equiv q₂) (h₂ : q₂.Equiv q₃) : q₁.Equiv q₃ := Eq.trans h₁ h₂

/-- Bridge: every `TranspQ` is a `CompQ` (with `u = t`).  The
    answer-equivalence is conditional on the base being dim-absent
    in the binder (the cubical typing premise that makes transport
    well-defined). -/
def TranspQ.toCompQ (q : TranspQ) : CompQ :=
  { env := q.env, binder := q.binder, body := q.body, φ := q.φ
  , u := q.t, t := q.t }

namespace TranspQ

/-- Transport classifiers — TranspQ versions of the body-shape and
    face-shape classifiers.  No `IsTransport` (every TranspQ is
    transport-shaped by construction).  Each tagged with
    `@[simp]` so they unfold under `simp`. -/
@[simp]
def IsConstLine (q : TranspQ) : Prop := q.body.dimAbsent q.binder = true
@[simp]
def IsFullFace (q : TranspQ) : Prop := q.φ = .top
@[simp]
def IsEmptyFace (q : TranspQ) : Prop := q.φ = .bot
@[simp]
def IsPathLine (q : TranspQ) : Prop :=
  ∃ A₀ a b, q.body = .path A₀ a b
@[simp]
def IsPiLine (q : TranspQ) : Prop :=
  ∃ domA codA, q.body = .pi domA codA
@[simp]
def IsSigmaLine (q : TranspQ) : Prop := ∃ A B, q.body = .sigma A B
@[simp]
def IsGlueLine (q : TranspQ) : Prop :=
  ∃ ψ T f fInv s r c A, q.body = .glue ψ T f fInv s r c A
@[simp]
def IsIndLine (q : TranspQ) : Prop := ∃ S params, q.body = .ind S params
@[simp]
def IsIntervalLine (q : TranspQ) : Prop := q.body = .interval
@[simp]
def IsUnivLine (q : TranspQ) : Prop := q.body = .univ

instance (q : TranspQ) : Decidable (IsConstLine q) :=
  inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true))
instance (q : TranspQ) : Decidable (IsFullFace q) :=
  inferInstanceAs (Decidable (q.φ = .top))
instance (q : TranspQ) : Decidable (IsEmptyFace q) :=
  inferInstanceAs (Decidable (q.φ = .bot))
instance (q : TranspQ) : Decidable (IsIntervalLine q) :=
  inferInstanceAs (Decidable (q.body = .interval))
instance (q : TranspQ) : Decidable (IsUnivLine q) :=
  inferInstanceAs (Decidable (q.body = .univ))

instance (q : TranspQ) : Decidable (IsPathLine q) :=
  match h : q.body with
  | .path A₀ a b => isTrue ⟨A₀, a, b, h⟩
  | .univ | .pi _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : TranspQ) : Decidable (IsPiLine q) :=
  match h : q.body with
  | .pi domA codA => isTrue ⟨domA, codA, h⟩
  | .univ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : TranspQ) : Decidable (IsSigmaLine q) :=
  match h : q.body with
  | .sigma A B => isTrue ⟨A, B, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : TranspQ) : Decidable (IsGlueLine q) :=
  match h : q.body with
  | .glue ψ T f fInv s r c A => isTrue ⟨ψ, T, f, fInv, s, r, c, A, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, _, _, _, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : TranspQ) : Decidable (IsIndLine q) :=
  match h : q.body with
  | .ind S params => isTrue ⟨S, params, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

-- ── Restated transport axioms — classifier-conditioned ──────────────────────

/-- T1 in question form: transport under a full face is identity. -/
@[simp]
theorem ask_of_full_face (q : TranspQ) (h : IsFullFace q) :
    q.ask = eval q.env q.t := by
  unfold ask; rw [show q.φ = .top from h]
  exact eval_transp_top q.env q.binder q.body q.t

/-- T2 in question form: transport along a constant line is identity. -/
@[simp]
theorem ask_of_const_line (q : TranspQ)
    (hC : IsConstLine q) (hφ : ¬ IsFullFace q) :
    q.ask = eval q.env q.t := by
  unfold ask
  exact eval_transp_const q.env q.binder q.body q.φ q.t hφ hC

/-- T3 in question form: transport along a path-typed line produces
    a `vPathTransp` closure (further reduction at endpoints via
    `vPApp` arms).

    Not in `question_simp` because the conclusion is an existential;
    use as `obtain ⟨A₀, a, b, hbody, hask⟩ := ask_of_path_line ...`. -/
theorem ask_of_path_line (q : TranspQ) (hP : IsPathLine q)
    (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) :
    ∃ A₀ a b, q.body = .path A₀ a b ∧
      q.ask = .vPathTransp q.env q.binder A₀ a b q.φ q.t := by
  obtain ⟨A₀, a, b, hbody⟩ := hP
  refine ⟨A₀, a, b, hbody, ?_⟩
  unfold ask
  rw [hbody]
  apply eval_transp_path q.env q.binder A₀ a b q.φ q.t hφ
  unfold IsConstLine at hC
  match hb : CType.dimAbsent q.binder (.path A₀ a b) with
  | true  => rw [hbody] at hC; exact absurd hb hC
  | false => rfl

/-- Π-line transport: produces a `vTranspFun` closure.  Derived from
    `eval_transp_pi`.

    Not in `question_simp` because the conclusion is an existential. -/
theorem ask_of_pi_line (q : TranspQ) (hP : IsPiLine q)
    (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) :
    ∃ domA codA, q.body = .pi domA codA ∧
      q.ask = .vTranspFun q.binder domA codA q.φ (eval q.env q.t) := by
  obtain ⟨domA, codA, hbody⟩ := hP
  refine ⟨domA, codA, hbody, ?_⟩
  unfold ask
  rw [hbody]
  apply eval_transp_pi q.env q.binder domA codA q.φ q.t hφ
  unfold IsConstLine at hC
  match hb : CType.dimAbsent q.binder (.pi domA codA) with
  | true  => rw [hbody] at hC; exact absurd hb hC
  | false => rfl

/-- Stuck case: non-path, non-glue, non-pi, non-constant line under a
    non-full face.  In our current `CType` universe this only fires
    on `.sigma` / `.ind` / `.interval` / `.univ` shapes that aren't
    already absorbed by `ask_of_const_line` (e.g., a `.sigma` line
    that genuinely varies — currently no such reduction). -/
theorem ask_of_stuck (q : TranspQ)
    (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q)
    (hP : ¬ IsPiLine q) (hPath : ¬ IsPathLine q) (hG : ¬ IsGlueLine q) :
    q.ask = .vneu (.ntransp q.binder q.body q.φ (eval q.env q.t)) := by
  unfold ask
  apply eval_transp_stuck q.env q.binder q.body q.φ q.t hφ
  · unfold IsConstLine at hC
    match hb : CType.dimAbsent q.binder q.body with
    | true  => exact absurd hb hC
    | false => rfl
  · intro domA codA hb; exact hP ⟨domA, codA, hb⟩
  · intro A₀ a b hb; exact hPath ⟨A₀, a, b, hb⟩
  · intro ψ T f fI s r c A hb; exact hG ⟨ψ, T, f, fI, s, r, c, A, hb⟩

/-- T2 specialised to `.interval`: the interval is dim-absent in
    every binder, so transport on `.interval` is always identity. -/
@[simp]
theorem ask_of_interval_line (q : TranspQ) (h : IsIntervalLine q) :
    q.ask = eval q.env q.t := by
  unfold ask
  rw [show q.body = .interval from h]
  exact eval_transp_interval q.env q.binder q.φ q.t

-- T2 specialised to `.ind` constant lines is just `ask_of_const_line`
-- — no separate alias needed.  The richer `.ind` lemma below extracts
-- the schema and parameters.

/-- Stuck `.ind` transport (non-trivial line): produces `ntransp`. -/
theorem ask_of_ind_stuck (q : TranspQ) (h : IsIndLine q)
    (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) :
    ∃ S params, q.body = .ind S params ∧
      q.ask = .vneu (.ntransp q.binder q.body q.φ (eval q.env q.t)) := by
  obtain ⟨S, params, hbody⟩ := h
  refine ⟨S, params, hbody, ?_⟩
  apply ask_of_stuck q hφ hC
  · intro ⟨_, _, hp⟩; rw [hp] at hbody; cases hbody
  · intro ⟨_, _, _, hp⟩; rw [hp] at hbody; cases hbody
  · intro ⟨_, _, _, _, _, _, _, _, hp⟩; rw [hp] at hbody; cases hbody

/-- T5 in question form: face congruence — semantically equal faces
    yield equivalent transport questions. -/
theorem ask_face_congr (q₁ q₂ : TranspQ)
    (h_env : q₁.env = q₂.env) (h_bind : q₁.binder = q₂.binder)
    (h_body : q₁.body = q₂.body) (h_t : q₁.t = q₂.t)
    (h_face : ∀ ε, q₁.φ.eval ε = q₂.φ.eval ε) :
    q₁.Equiv q₂ := by
  unfold Equiv ask
  rw [h_env, h_bind, h_body, h_t]
  exact eval_transp_face_congr q₂.env q₂.binder q₂.body q₁.φ q₂.φ q₂.t h_face

/-- Bridge: on the full-face arm, `TranspQ.toCompQ q` has the same
    `ask` as the transport itself, provided the base is dim-absent in
    the line binder.

    **Why only the full-face case.**  On `φ = .top`:
      · transport: `eval_transp_top` → `eval env t`.
      · comp:      `eval_comp_top` → `eval env (t.substDim binder .one)`.
    Under `t.dimAbsent binder = true`, the substitution is identity
    and both sides agree.

    On non-trivial faces with a constant body:
      · transport: `eval_transp_const` → `eval env t`.
      · comp:      `eval_comp_const` → `vHCompValue body φ … …`,
                   which is a non-trivial value for non-Π bodies.
    So the two answers genuinely diverge in the general non-trivial-
    face case.  The bridge is therefore restricted to the full-face
    arm; broader reconciliations live in the engine's typed totality
    proofs (REL3+). -/
theorem toCompQ_ask_eq_ask_full_face (q : TranspQ)
    (hφ : IsFullFace q) (hi : q.t.dimAbsent q.binder = true) :
    q.toCompQ.ask = q.ask := by
  rw [ask_of_full_face q hφ]
  show eval q.env (.comp q.binder q.body q.φ q.t q.t) = eval q.env q.t
  rw [show q.φ = .top from hφ]
  rw [eval_comp_top q.env q.binder q.body q.t q.t]
  congr 1
  exact CTerm.substDim_of_absent q.binder .one q.t hi

end TranspQ

-- ──────────────────────────────────────────────────────────────────────────
-- HCompQ — homogeneous-comp question (value-level)
-- ──────────────────────────────────────────────────────────────────────────
--
-- Homogeneous composition `hcomp A φ tube base` lives at the *value*
-- level: the engine's `vHCompValue : CType → FaceFormula → CVal → CVal → CVal`
-- consumes already-evaluated `tube` and `base`.  This is the one
-- question that doesn't take an environment — by the time you've
-- reduced to hcomp, evaluation has already happened.

/-- Homogeneous composition question.  The "constant-line" CompQ
    that has been reduced one step further by extracting the tube
    as a `vplam`-shaped value. -/
structure HCompQ where
  body : CType
  φ    : FaceFormula
  tube : CVal
  base : CVal

def HCompQ.ask (q : HCompQ) : CVal := vHCompValue q.body q.φ q.tube q.base

def HCompQ.Equiv (q₁ q₂ : HCompQ) : Prop := q₁.ask = q₂.ask

@[refl] theorem HCompQ.Equiv.refl (q : HCompQ) : q.Equiv q := rfl
@[symm] theorem HCompQ.Equiv.symm {q₁ q₂ : HCompQ}
    (h : q₁.Equiv q₂) : q₂.Equiv q₁ := Eq.symm h
theorem HCompQ.Equiv.trans {q₁ q₂ q₃ : HCompQ}
    (h₁ : q₁.Equiv q₂) (h₂ : q₂.Equiv q₃) : q₁.Equiv q₃ := Eq.trans h₁ h₂

namespace HCompQ

@[simp]
def IsFullFace (q : HCompQ) : Prop := q.φ = .top
@[simp]
def IsPiLine (q : HCompQ) : Prop := ∃ domA codA, q.body = .pi domA codA

instance (q : HCompQ) : Decidable (IsFullFace q) :=
  inferInstanceAs (Decidable (q.φ = .top))

instance (q : HCompQ) : Decidable (IsPiLine q) :=
  match h : q.body with
  | .pi domA codA => isTrue ⟨domA, codA, h⟩
  | .univ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

/-- Full-face hcomp: tube evaluated at `1` is the answer. -/
@[simp]
theorem ask_of_full_face (q : HCompQ) (h : IsFullFace q) :
    q.ask = vPApp q.tube .one := by
  unfold ask; rw [show q.φ = .top from h]
  exact vHCompValue_top q.body q.tube q.base

/-- Π-line hcomp: packages into a `vHCompFun` closure.  Not in
    `question_simp` (existential conclusion). -/
theorem ask_of_pi_line (q : HCompQ) (hP : IsPiLine q)
    (hφ : ¬ IsFullFace q) :
    ∃ domA codA, q.body = .pi domA codA ∧
      q.ask = .vHCompFun codA q.φ q.tube q.base := by
  obtain ⟨domA, codA, hbody⟩ := hP
  refine ⟨domA, codA, hbody, ?_⟩
  unfold ask; rw [hbody]
  exact vHCompValue_pi domA codA q.φ q.tube q.base hφ

/-- Stuck hcomp: non-Π body under a non-full face produces `nhcomp`. -/
theorem ask_of_stuck (q : HCompQ)
    (hφ : ¬ IsFullFace q) (hP : ¬ IsPiLine q) :
    q.ask = .vneu (.nhcomp q.body q.φ q.tube q.base) := by
  unfold ask
  apply vHCompValue_stuck q.body q.φ q.tube q.base hφ
  intro domA codA hb; exact hP ⟨domA, codA, hb⟩

end HCompQ

-- ──────────────────────────────────────────────────────────────────────────
-- CompNQ — multi-clause heterogeneous-comp question
-- ──────────────────────────────────────────────────────────────────────────
--
-- `compNⁱ A [φ_1 ↦ u_1, …, φ_n ↦ u_n] t` — a partial element defined
-- over the union of clause faces.  Its reduction depends on the
-- clauses' shape (any `.top`?  all `.bot`?  exactly one live?  many?).

/-- Multi-clause heterogeneous-comp question. -/
structure CompNQ where
  env     : CEnv
  binder  : DimVar
  body    : CType
  clauses : List (FaceFormula × CTerm)
  t       : CTerm

def CompNQ.ask (q : CompNQ) : CVal :=
  vCompNAtTerm q.env q.binder q.body q.clauses q.t

def CompNQ.Equiv (q₁ q₂ : CompNQ) : Prop := q₁.ask = q₂.ask

@[refl] theorem CompNQ.Equiv.refl (q : CompNQ) : q.Equiv q := rfl
@[symm] theorem CompNQ.Equiv.symm {q₁ q₂ : CompNQ}
    (h : q₁.Equiv q₂) : q₂.Equiv q₁ := Eq.symm h
theorem CompNQ.Equiv.trans {q₁ q₂ q₃ : CompNQ}
    (h₁ : q₁.Equiv q₂) (h₂ : q₂.Equiv q₃) : q₁.Equiv q₃ := Eq.trans h₁ h₂

namespace CompNQ

/-- Bool-valued: does some clause have face `.top`?  Used to decide
    whether `vCompNAtTerm` will fire the top-clause arm. -/
def hasTopClause (q : CompNQ) : Bool :=
  q.clauses.any fun ⟨φ, _⟩ => match φ with | .top => true | _ => false

/-- The clause list contains some clause whose face is `.top` —
    that clause's body fires at `binder := 1`. -/
def HasTopClause (q : CompNQ) : Prop := q.hasTopClause = true

instance (q : CompNQ) : Decidable (HasTopClause q) :=
  inferInstanceAs (Decidable (q.hasTopClause = true))

/-- The list of "live" clauses: those whose face is not `.bot`. -/
def liveClauses (q : CompNQ) : List (FaceFormula × CTerm) :=
  q.clauses.filter fun ⟨φ, _⟩ => match φ with | .bot => false | _ => true

/-- Every clause has face `.bot` (or the list is empty) — no live
    contributions, the question reduces to plain transport on `t`. -/
def AllBotOrEmpty (q : CompNQ) : Prop := q.liveClauses = []

instance (q : CompNQ) : Decidable (AllBotOrEmpty q) :=
  inferInstanceAs (Decidable (q.liveClauses = []))

/-- Exactly one live clause — the question reduces to a single
    `CompQ` on that clause. -/
def IsSingleLive (q : CompNQ) : Prop := ∃ p, q.liveClauses = [p]

instance (q : CompNQ) : Decidable (IsSingleLive q) :=
  match h : q.liveClauses with
  | [p] => isTrue ⟨p, h⟩
  | [] => isFalse (fun ⟨_, hp⟩ => by rw [h] at hp; cases hp)
  | _ :: _ :: _ => isFalse (fun ⟨_, hp⟩ => by rw [h] at hp; cases hp)

-- ── Restated `vCompNAtTerm_def` — one theorem per arm ──────────────────────

/-- The CompN reduction "anatomy" axiom restated through the
    classifier vocabulary: every CompN question's answer is one of
    four shapes, decidable from `HasTopClause` / `AllBotOrEmpty` /
    `IsSingleLive`. -/
theorem ask_def (q : CompNQ) :
    q.ask =
      match q.clauses.find?
        (fun ⟨φ, _⟩ => match φ with | .top => true | _ => false) with
      | some ⟨_, u⟩ => eval q.env (u.substDim q.binder .one)
      | none =>
        let live := q.clauses.filter
          (fun ⟨φ, _⟩ => match φ with | .bot => false | _ => true)
        match live with
        | []        => eval q.env (.transp q.binder q.body .bot q.t)
        | [⟨φ, u⟩] => vCompAtTerm q.env q.binder q.body φ u q.t
        | _         => .vneu (.ncompN q.env q.binder q.body
                          (live.map (fun ⟨φ, u⟩ => (φ, eval q.env u)))
                          (eval q.env q.t)) := by
  unfold ask
  exact vCompNAtTerm_def q.env q.binder q.body q.clauses q.t

end CompNQ

end Question

-- ──────────────────────────────────────────────────────────────────────────
-- `question_simp` simp-set sanity checks
-- ──────────────────────────────────────────────────────────────────────────
-- Each `@[simp]`-tagged classifier definition or
-- classifier-conditioned theorem is reachable via `simp`.
-- These examples verify the named simp-set composes — no special
-- tactic involved, just Lean's standard `simp`.  Anyone wanting a
-- different reduction order or extra lemmas writes
-- `simp [question_simp, my_extras]` — no opinion baked in.
--
-- (The earlier `cubical_simp` macros were removed: they baked in a
-- specific lemma list with a fixed expansion order.  Use the
-- declarative simp set instead.)

example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    let q : Question.CompQ := ⟨env, i, A, .top, u, t⟩
    q.ask = eval env (u.substDim i .one) := by
  simp

example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    let q : Question.CompQ := ⟨env, i, A, .bot, u, t⟩
    q.ask = eval env (.transp i A .bot t) := by
  simp

/-- Transport-shaped (`u = t`) interval-line CompQ under a full
    face with a dim-absent base reduces to `eval env t`. -/
example (env : CEnv) (i : DimVar) (t : CTerm)
    (hi : t.dimAbsent i = true) :
    (Question.CompQ.ofTransp env i .interval .top t).ask = eval env t := by
  apply Question.CompQ.ask_of_transport_full_face
  · rfl
  · rfl
  · exact hi

example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
    let q : Question.TranspQ := ⟨env, i, A, .top, t⟩
    q.ask = eval env t := by
  simp

example (env : CEnv) (i : DimVar) (t : CTerm) :
    let q : Question.TranspQ := ⟨env, i, .interval, .bot, t⟩
    q.ask = eval env t := by
  simp

example (A : CType) (tube base : CVal) :
    let q : Question.HCompQ := ⟨A, .top, tube, base⟩
    q.ask = vPApp tube .one := by
  simp