From 271b47102e620f73a224b69ac6833ffa495397d2 Mon Sep 17 00:00:00 2001
From: Maximus Gorog <mgorog@gmail.com>
Date: Fri, 1 May 2026 00:34:14 -0600
Subject: [PATCH] QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Lands the foundational DecidableEq machinery and the @[simp]-
based question-form routing in one go (per project discipline:
no shortcuts, no compat shims).

CubicalTransport/DecEq.lean (new, ~290 lines):
- Mutual decEq for the 5-way AST block (CType, CTerm, CTypeArg,
  CtorSpec, CTypeSchema) plus list/clause/branch helpers
  (decEqListCType, decEqListCTerm, decEqListCTypeArg,
  decEqListCtorSpec, decEqClauses, decEqBranches).
- Returns Decidable (a = b) directly; uses OR-patterns for
  cross-constructor mismatches, discharged uniformly via cases.
- Five DecidableEq instances declared post-block.
- Lean 4 deriving doesn't support mutual inductives; manual
  decEq is the canonical approach.

CubicalTransport/Interval.lean: deriving DecidableEq on DimExpr.
CubicalTransport/Face.lean: deriving DecidableEq on FaceFormula.

CubicalTransport/Question.lean:
- All 11 classifier Decidable instances now land:
    IsConstLine, IsFullFace, IsEmptyFace, IsTransport,
    IsIntervalLine, IsUnivLine — direct from DecidableEq.
    IsPathLine, IsPiLine, IsSigmaLine, IsGlueLine, IsIndLine —
    via match h : q.body with on the head constructor +
    existential-witness reconstruction in the isTrue arm.
- @[simp] tags on ask_of_full_face / ask_of_empty_face /
  ask_of_const_line / ask_of_transport_full_face — the Level 2
  routing through CompQ.Equiv.
- Three example proofs at end of file demonstrating that the
  simp-set composes (full-face C1, empty-face C2, transport-
  shaped interval-line reduction).

CubicalTransport/FFITest.lean: 6 new classifier-decidability
smoke tests (IsFullFace, IsTransport×2, IsPiLine, IsIntervalLine).
Test count: 84 → 89 passing.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 CubicalTransport.lean          |   1 +
 CubicalTransport/DecEq.lean    | 399 +++++++++++++++++++++++++++++++++
 CubicalTransport/FFITest.lean  |  32 ++-
 CubicalTransport/Face.lean     |   2 +-
 CubicalTransport/Interval.lean |   2 +-
 CubicalTransport/Question.lean |  94 +++++++-
 CubicalTransport/Syntax.lean   |   4 +
 7 files changed, 524 insertions(+), 10 deletions(-)
 create mode 100644 CubicalTransport/DecEq.lean

diff --git a/CubicalTransport.lean b/CubicalTransport.lean
index ea72dc1..8eaf001 100644
--- a/CubicalTransport.lean
+++ b/CubicalTransport.lean
@@ -1,6 +1,7 @@
 import CubicalTransport.Interval
 import CubicalTransport.Face
 import CubicalTransport.Syntax
+import CubicalTransport.DecEq
 import CubicalTransport.Subst
 import CubicalTransport.DimLine
 import CubicalTransport.Typing
diff --git a/CubicalTransport/DecEq.lean b/CubicalTransport/DecEq.lean
new file mode 100644
index 0000000..f6b0385
--- /dev/null
+++ b/CubicalTransport/DecEq.lean
@@ -0,0 +1,399 @@
+/-
+  CubicalTransport.DecEq
+  ======================
+  Decidable equality for the 5-way mutual block (`CType`, `CTerm`,
+  `CTypeArg`, `CtorSpec`, `CTypeSchema`) plus the list/pair helper
+  shapes that appear inside it.
+
+  Lean 4's `deriving instance DecidableEq` does not currently support
+  mutual inductives — has to be written manually.  The mutual `decEq`
+  block returns `Decidable (a = b)` directly; instances are then
+  declared post-hoc.
+
+  Imports `CubicalTransport.Syntax` and depends on the `DecidableEq`
+  instances for `DimVar`, `DimExpr`, and `FaceFormula` (added in
+  `Interval.lean` / `Face.lean`).
+
+  Used by `CubicalTransport.Question` for syntactic-classifier
+  decidability (`IsFullFace`, `IsEmptyFace`, `IsIntervalLine`,
+  `IsUnivLine`, `IsTransport`, `IsPathLine`, …).  Cells-spec /
+  paideia downstream consumers also benefit (they want to compare
+  AST nodes when normalising / dispatching).
+-/
+
+import CubicalTransport.Syntax
+
+namespace CubicalTransport.DecEq
+
+-- ── Mutual decEq block ──────────────────────────────────────────────────────
+-- Every Decidable (a = b) on the 5 AST types and their list/pair
+-- helpers lives here.  The block is structurally recursive on the AST
+-- subterms and uses Lean's automatic recognition of OR-patterns to
+-- collapse cross-constructor mismatches into a single `isFalse` arm.
+
+mutual
+
+def CType.decEq : (a b : CType) → Decidable (a = b)
+  | .univ, .univ => isTrue rfl
+  | .pi A B, .pi A' B' =>
+      match CType.decEq A A', CType.decEq B B' with
+      | isTrue hA, isTrue hB => isTrue (by rw [hA, hB])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .path A a b, .path A' a' b' =>
+      match CType.decEq A A', CTerm.decEq a a', CTerm.decEq b b' with
+      | isTrue hA, isTrue ha, isTrue hb => isTrue (by rw [hA, ha, hb])
+      | isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .sigma A B, .sigma A' B' =>
+      match CType.decEq A A', CType.decEq B B' with
+      | isTrue hA, isTrue hB => isTrue (by rw [hA, hB])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .glue ψ T f fInv s r c A, .glue ψ' T' f' fInv' s' r' c' A' =>
+      if hψ : ψ = ψ' then
+        match CType.decEq T T', CTerm.decEq f f', CTerm.decEq fInv fInv',
+              CTerm.decEq s s', CTerm.decEq r r', CTerm.decEq c c',
+              CType.decEq A A' with
+        | isTrue hT, isTrue hf, isTrue hfI, isTrue hs, isTrue hr, isTrue hc, isTrue hA =>
+            isTrue (by rw [hψ, hT, hf, hfI, hs, hr, hc, hA])
+        | isFalse h, _, _, _, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h, _, _, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, isFalse h, _, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, _, isFalse h, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, _, _, isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, _, _, _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, _, _, _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else
+        isFalse (fun heq => hψ (by cases heq; rfl))
+  | .ind S ps, .ind S' ps' =>
+      match CTypeSchema.decEq S S', decEqListCType ps ps' with
+      | isTrue hS, isTrue hp => isTrue (by rw [hS, hp])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .interval, .interval => isTrue rfl
+  -- Cross-constructor mismatches.  Each row enumerates the (a, b)
+  -- shapes where the head constructors differ; `cases heq` discharges
+  -- because the eliminator treats them as inhabited-but-equal-only-
+  -- between-same-constructor.
+  | .univ, .pi _ _ | .univ, .path _ _ _ | .univ, .sigma _ _
+  | .univ, .glue _ _ _ _ _ _ _ _ | .univ, .ind _ _ | .univ, .interval
+  | .pi _ _, .univ | .pi _ _, .path _ _ _ | .pi _ _, .sigma _ _
+  | .pi _ _, .glue _ _ _ _ _ _ _ _ | .pi _ _, .ind _ _ | .pi _ _, .interval
+  | .path _ _ _, .univ | .path _ _ _, .pi _ _ | .path _ _ _, .sigma _ _
+  | .path _ _ _, .glue _ _ _ _ _ _ _ _ | .path _ _ _, .ind _ _ | .path _ _ _, .interval
+  | .sigma _ _, .univ | .sigma _ _, .pi _ _ | .sigma _ _, .path _ _ _
+  | .sigma _ _, .glue _ _ _ _ _ _ _ _ | .sigma _ _, .ind _ _ | .sigma _ _, .interval
+  | .glue _ _ _ _ _ _ _ _, .univ | .glue _ _ _ _ _ _ _ _, .pi _ _
+  | .glue _ _ _ _ _ _ _ _, .path _ _ _ | .glue _ _ _ _ _ _ _ _, .sigma _ _
+  | .glue _ _ _ _ _ _ _ _, .ind _ _ | .glue _ _ _ _ _ _ _ _, .interval
+  | .ind _ _, .univ | .ind _ _, .pi _ _ | .ind _ _, .path _ _ _
+  | .ind _ _, .sigma _ _ | .ind _ _, .glue _ _ _ _ _ _ _ _ | .ind _ _, .interval
+  | .interval, .univ | .interval, .pi _ _ | .interval, .path _ _ _
+  | .interval, .sigma _ _ | .interval, .glue _ _ _ _ _ _ _ _ | .interval, .ind _ _ =>
+      isFalse (fun heq => by cases heq)
+
+def CTerm.decEq : (a b : CTerm) → Decidable (a = b)
+  | .var x, .var y =>
+      if h : x = y then isTrue (by rw [h]) else isFalse (fun heq => h (by cases heq; rfl))
+  | .lam x t, .lam y u =>
+      if hx : x = y then
+        match CTerm.decEq t u with
+        | isTrue ht => isTrue (by rw [hx, ht])
+        | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else
+        isFalse (fun heq => hx (by cases heq; rfl))
+  | .app f a, .app f' a' =>
+      match CTerm.decEq f f', CTerm.decEq a a' with
+      | isTrue hf, isTrue ha => isTrue (by rw [hf, ha])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .plam i t, .plam j u =>
+      if hi : i = j then
+        match CTerm.decEq t u with
+        | isTrue ht => isTrue (by rw [hi, ht])
+        | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else
+        isFalse (fun heq => hi (by cases heq; rfl))
+  | .papp t r, .papp u s =>
+      if hr : r = s then
+        match CTerm.decEq t u with
+        | isTrue ht => isTrue (by rw [hr, ht])
+        | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else
+        isFalse (fun heq => hr (by cases heq; rfl))
+  | .transp i A φ t, .transp j B ψ u =>
+      if hi : i = j then if hφ : φ = ψ then
+        match CType.decEq A B, CTerm.decEq t u with
+        | isTrue hA, isTrue ht => isTrue (by rw [hi, hA, hφ, ht])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hφ (by cases heq; rfl))
+      else isFalse (fun heq => hi (by cases heq; rfl))
+  | .comp i A φ u t, .comp j B ψ u' t' =>
+      if hi : i = j then if hφ : φ = ψ then
+        match CType.decEq A B, CTerm.decEq u u', CTerm.decEq t t' with
+        | isTrue hA, isTrue hu, isTrue ht => isTrue (by rw [hi, hA, hφ, hu, ht])
+        | isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hφ (by cases heq; rfl))
+      else isFalse (fun heq => hi (by cases heq; rfl))
+  | .compN i A cs t, .compN j B cs' t' =>
+      if hi : i = j then
+        match CType.decEq A B, decEqClauses cs cs', CTerm.decEq t t' with
+        | isTrue hA, isTrue hc, isTrue ht => isTrue (by rw [hi, hA, hc, ht])
+        | isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hi (by cases heq; rfl))
+  | .glueIn φ t a, .glueIn ψ u b =>
+      if hφ : φ = ψ then
+        match CTerm.decEq t u, CTerm.decEq a b with
+        | isTrue ht, isTrue ha => isTrue (by rw [hφ, ht, ha])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hφ (by cases heq; rfl))
+  | .unglue φ f g, .unglue ψ f' g' =>
+      if hφ : φ = ψ then
+        match CTerm.decEq f f', CTerm.decEq g g' with
+        | isTrue hf, isTrue hg => isTrue (by rw [hφ, hf, hg])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hφ (by cases heq; rfl))
+  | .pair a b, .pair a' b' =>
+      match CTerm.decEq a a', CTerm.decEq b b' with
+      | isTrue ha, isTrue hb => isTrue (by rw [ha, hb])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .fst t, .fst u =>
+      match CTerm.decEq t u with
+      | isTrue ht => isTrue (by rw [ht])
+      | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .snd t, .snd u =>
+      match CTerm.decEq t u with
+      | isTrue ht => isTrue (by rw [ht])
+      | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .dimExpr r, .dimExpr s =>
+      if h : r = s then isTrue (by rw [h]) else isFalse (fun heq => h (by cases heq; rfl))
+  | .ctor S c ps as, .ctor S' c' ps' as' =>
+      if hc : c = c' then
+        match CTypeSchema.decEq S S', decEqListCType ps ps', decEqListCTerm as as' with
+        | isTrue hS, isTrue hp, isTrue ha => isTrue (by rw [hS, hc, hp, ha])
+        | isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hc (by cases heq; rfl))
+  | .indElim S ps m bs t, .indElim S' ps' m' bs' t' =>
+      match CTypeSchema.decEq S S', decEqListCType ps ps',
+            CTerm.decEq m m', decEqBranches bs bs', CTerm.decEq t t' with
+      | isTrue hS, isTrue hp, isTrue hm, isTrue hb, isTrue ht =>
+          isTrue (by rw [hS, hp, hm, hb, ht])
+      | isFalse h, _, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h, _, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, _, isFalse h, _, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, _, _, isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, _, _, _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  -- Cross-constructor mismatches.  Lean discharges via `cases heq`.
+  | .var _, .lam _ _ | .var _, .app _ _ | .var _, .plam _ _ | .var _, .papp _ _
+  | .var _, .transp _ _ _ _ | .var _, .comp _ _ _ _ _ | .var _, .compN _ _ _ _
+  | .var _, .glueIn _ _ _ | .var _, .unglue _ _ _ | .var _, .pair _ _
+  | .var _, .fst _ | .var _, .snd _ | .var _, .dimExpr _ | .var _, .ctor _ _ _ _
+  | .var _, .indElim _ _ _ _ _
+  | .lam _ _, .var _ | .lam _ _, .app _ _ | .lam _ _, .plam _ _ | .lam _ _, .papp _ _
+  | .lam _ _, .transp _ _ _ _ | .lam _ _, .comp _ _ _ _ _ | .lam _ _, .compN _ _ _ _
+  | .lam _ _, .glueIn _ _ _ | .lam _ _, .unglue _ _ _ | .lam _ _, .pair _ _
+  | .lam _ _, .fst _ | .lam _ _, .snd _ | .lam _ _, .dimExpr _ | .lam _ _, .ctor _ _ _ _
+  | .lam _ _, .indElim _ _ _ _ _
+  | .app _ _, .var _ | .app _ _, .lam _ _ | .app _ _, .plam _ _ | .app _ _, .papp _ _
+  | .app _ _, .transp _ _ _ _ | .app _ _, .comp _ _ _ _ _ | .app _ _, .compN _ _ _ _
+  | .app _ _, .glueIn _ _ _ | .app _ _, .unglue _ _ _ | .app _ _, .pair _ _
+  | .app _ _, .fst _ | .app _ _, .snd _ | .app _ _, .dimExpr _ | .app _ _, .ctor _ _ _ _
+  | .app _ _, .indElim _ _ _ _ _
+  | .plam _ _, .var _ | .plam _ _, .lam _ _ | .plam _ _, .app _ _ | .plam _ _, .papp _ _
+  | .plam _ _, .transp _ _ _ _ | .plam _ _, .comp _ _ _ _ _ | .plam _ _, .compN _ _ _ _
+  | .plam _ _, .glueIn _ _ _ | .plam _ _, .unglue _ _ _ | .plam _ _, .pair _ _
+  | .plam _ _, .fst _ | .plam _ _, .snd _ | .plam _ _, .dimExpr _ | .plam _ _, .ctor _ _ _ _
+  | .plam _ _, .indElim _ _ _ _ _
+  | .papp _ _, .var _ | .papp _ _, .lam _ _ | .papp _ _, .app _ _ | .papp _ _, .plam _ _
+  | .papp _ _, .transp _ _ _ _ | .papp _ _, .comp _ _ _ _ _ | .papp _ _, .compN _ _ _ _
+  | .papp _ _, .glueIn _ _ _ | .papp _ _, .unglue _ _ _ | .papp _ _, .pair _ _
+  | .papp _ _, .fst _ | .papp _ _, .snd _ | .papp _ _, .dimExpr _ | .papp _ _, .ctor _ _ _ _
+  | .papp _ _, .indElim _ _ _ _ _
+  | .transp _ _ _ _, .var _ | .transp _ _ _ _, .lam _ _ | .transp _ _ _ _, .app _ _
+  | .transp _ _ _ _, .plam _ _ | .transp _ _ _ _, .papp _ _ | .transp _ _ _ _, .comp _ _ _ _ _
+  | .transp _ _ _ _, .compN _ _ _ _ | .transp _ _ _ _, .glueIn _ _ _
+  | .transp _ _ _ _, .unglue _ _ _ | .transp _ _ _ _, .pair _ _ | .transp _ _ _ _, .fst _
+  | .transp _ _ _ _, .snd _ | .transp _ _ _ _, .dimExpr _ | .transp _ _ _ _, .ctor _ _ _ _
+  | .transp _ _ _ _, .indElim _ _ _ _ _
+  | .comp _ _ _ _ _, .var _ | .comp _ _ _ _ _, .lam _ _ | .comp _ _ _ _ _, .app _ _
+  | .comp _ _ _ _ _, .plam _ _ | .comp _ _ _ _ _, .papp _ _ | .comp _ _ _ _ _, .transp _ _ _ _
+  | .comp _ _ _ _ _, .compN _ _ _ _ | .comp _ _ _ _ _, .glueIn _ _ _
+  | .comp _ _ _ _ _, .unglue _ _ _ | .comp _ _ _ _ _, .pair _ _
+  | .comp _ _ _ _ _, .fst _ | .comp _ _ _ _ _, .snd _ | .comp _ _ _ _ _, .dimExpr _
+  | .comp _ _ _ _ _, .ctor _ _ _ _ | .comp _ _ _ _ _, .indElim _ _ _ _ _
+  | .compN _ _ _ _, .var _ | .compN _ _ _ _, .lam _ _ | .compN _ _ _ _, .app _ _
+  | .compN _ _ _ _, .plam _ _ | .compN _ _ _ _, .papp _ _ | .compN _ _ _ _, .transp _ _ _ _
+  | .compN _ _ _ _, .comp _ _ _ _ _ | .compN _ _ _ _, .glueIn _ _ _
+  | .compN _ _ _ _, .unglue _ _ _ | .compN _ _ _ _, .pair _ _ | .compN _ _ _ _, .fst _
+  | .compN _ _ _ _, .snd _ | .compN _ _ _ _, .dimExpr _ | .compN _ _ _ _, .ctor _ _ _ _
+  | .compN _ _ _ _, .indElim _ _ _ _ _
+  | .glueIn _ _ _, .var _ | .glueIn _ _ _, .lam _ _ | .glueIn _ _ _, .app _ _
+  | .glueIn _ _ _, .plam _ _ | .glueIn _ _ _, .papp _ _ | .glueIn _ _ _, .transp _ _ _ _
+  | .glueIn _ _ _, .comp _ _ _ _ _ | .glueIn _ _ _, .compN _ _ _ _
+  | .glueIn _ _ _, .unglue _ _ _ | .glueIn _ _ _, .pair _ _ | .glueIn _ _ _, .fst _
+  | .glueIn _ _ _, .snd _ | .glueIn _ _ _, .dimExpr _ | .glueIn _ _ _, .ctor _ _ _ _
+  | .glueIn _ _ _, .indElim _ _ _ _ _
+  | .unglue _ _ _, .var _ | .unglue _ _ _, .lam _ _ | .unglue _ _ _, .app _ _
+  | .unglue _ _ _, .plam _ _ | .unglue _ _ _, .papp _ _ | .unglue _ _ _, .transp _ _ _ _
+  | .unglue _ _ _, .comp _ _ _ _ _ | .unglue _ _ _, .compN _ _ _ _
+  | .unglue _ _ _, .glueIn _ _ _ | .unglue _ _ _, .pair _ _ | .unglue _ _ _, .fst _
+  | .unglue _ _ _, .snd _ | .unglue _ _ _, .dimExpr _ | .unglue _ _ _, .ctor _ _ _ _
+  | .unglue _ _ _, .indElim _ _ _ _ _
+  | .pair _ _, .var _ | .pair _ _, .lam _ _ | .pair _ _, .app _ _ | .pair _ _, .plam _ _
+  | .pair _ _, .papp _ _ | .pair _ _, .transp _ _ _ _ | .pair _ _, .comp _ _ _ _ _
+  | .pair _ _, .compN _ _ _ _ | .pair _ _, .glueIn _ _ _ | .pair _ _, .unglue _ _ _
+  | .pair _ _, .fst _ | .pair _ _, .snd _ | .pair _ _, .dimExpr _ | .pair _ _, .ctor _ _ _ _
+  | .pair _ _, .indElim _ _ _ _ _
+  | .fst _, .var _ | .fst _, .lam _ _ | .fst _, .app _ _ | .fst _, .plam _ _
+  | .fst _, .papp _ _ | .fst _, .transp _ _ _ _ | .fst _, .comp _ _ _ _ _
+  | .fst _, .compN _ _ _ _ | .fst _, .glueIn _ _ _ | .fst _, .unglue _ _ _
+  | .fst _, .pair _ _ | .fst _, .snd _ | .fst _, .dimExpr _ | .fst _, .ctor _ _ _ _
+  | .fst _, .indElim _ _ _ _ _
+  | .snd _, .var _ | .snd _, .lam _ _ | .snd _, .app _ _ | .snd _, .plam _ _
+  | .snd _, .papp _ _ | .snd _, .transp _ _ _ _ | .snd _, .comp _ _ _ _ _
+  | .snd _, .compN _ _ _ _ | .snd _, .glueIn _ _ _ | .snd _, .unglue _ _ _
+  | .snd _, .pair _ _ | .snd _, .fst _ | .snd _, .dimExpr _ | .snd _, .ctor _ _ _ _
+  | .snd _, .indElim _ _ _ _ _
+  | .dimExpr _, .var _ | .dimExpr _, .lam _ _ | .dimExpr _, .app _ _
+  | .dimExpr _, .plam _ _ | .dimExpr _, .papp _ _ | .dimExpr _, .transp _ _ _ _
+  | .dimExpr _, .comp _ _ _ _ _ | .dimExpr _, .compN _ _ _ _
+  | .dimExpr _, .glueIn _ _ _ | .dimExpr _, .unglue _ _ _ | .dimExpr _, .pair _ _
+  | .dimExpr _, .fst _ | .dimExpr _, .snd _ | .dimExpr _, .ctor _ _ _ _
+  | .dimExpr _, .indElim _ _ _ _ _
+  | .ctor _ _ _ _, .var _ | .ctor _ _ _ _, .lam _ _ | .ctor _ _ _ _, .app _ _
+  | .ctor _ _ _ _, .plam _ _ | .ctor _ _ _ _, .papp _ _ | .ctor _ _ _ _, .transp _ _ _ _
+  | .ctor _ _ _ _, .comp _ _ _ _ _ | .ctor _ _ _ _, .compN _ _ _ _
+  | .ctor _ _ _ _, .glueIn _ _ _ | .ctor _ _ _ _, .unglue _ _ _ | .ctor _ _ _ _, .pair _ _
+  | .ctor _ _ _ _, .fst _ | .ctor _ _ _ _, .snd _ | .ctor _ _ _ _, .dimExpr _
+  | .ctor _ _ _ _, .indElim _ _ _ _ _
+  | .indElim _ _ _ _ _, .var _ | .indElim _ _ _ _ _, .lam _ _ | .indElim _ _ _ _ _, .app _ _
+  | .indElim _ _ _ _ _, .plam _ _ | .indElim _ _ _ _ _, .papp _ _
+  | .indElim _ _ _ _ _, .transp _ _ _ _ | .indElim _ _ _ _ _, .comp _ _ _ _ _
+  | .indElim _ _ _ _ _, .compN _ _ _ _ | .indElim _ _ _ _ _, .glueIn _ _ _
+  | .indElim _ _ _ _ _, .unglue _ _ _ | .indElim _ _ _ _ _, .pair _ _
+  | .indElim _ _ _ _ _, .fst _ | .indElim _ _ _ _ _, .snd _ | .indElim _ _ _ _ _, .dimExpr _
+  | .indElim _ _ _ _ _, .ctor _ _ _ _ =>
+      isFalse (fun heq => by cases heq)
+
+def CTypeArg.decEq : (a b : CTypeArg) → Decidable (a = b)
+  | .type A, .type B =>
+      match CType.decEq A B with
+      | isTrue h => isTrue (by rw [h])
+      | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+  | .param i, .param j =>
+      if h : i = j then isTrue (by rw [h]) else isFalse (fun heq => h (by cases heq; rfl))
+  | .self, .self => isTrue rfl
+  | .dim, .dim => isTrue rfl
+  | .type _, .param _ | .type _, .self | .type _, .dim
+  | .param _, .type _ | .param _, .self | .param _, .dim
+  | .self, .type _ | .self, .param _ | .self, .dim
+  | .dim, .type _ | .dim, .param _ | .dim, .self =>
+      isFalse (fun heq => by cases heq)
+
+def CtorSpec.decEq : (a b : CtorSpec) → Decidable (a = b)
+  | .mk n as bs, .mk n' as' bs' =>
+      if hn : n = n' then
+        match decEqListCTypeArg as as', decEqClauses bs bs' with
+        | isTrue ha, isTrue hb => isTrue (by rw [hn, ha, hb])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hn (by cases heq; rfl))
+
+def CTypeSchema.decEq : (a b : CTypeSchema) → Decidable (a = b)
+  | .mk n np cs, .mk n' np' cs' =>
+      if hn : n = n' then if hnp : np = np' then
+        match decEqListCtorSpec cs cs' with
+        | isTrue hc => isTrue (by rw [hn, hnp, hc])
+        | isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hnp (by cases heq; rfl))
+      else isFalse (fun heq => hn (by cases heq; rfl))
+
+-- ── List / clause / branch helpers ──────────────────────────────────────────
+
+def decEqListCType : (xs ys : List CType) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | x :: xs, y :: ys =>
+      match CType.decEq x y, decEqListCType xs ys with
+      | isTrue hx, isTrue hxs => isTrue (by rw [hx, hxs])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+
+def decEqListCTerm : (xs ys : List CTerm) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | x :: xs, y :: ys =>
+      match CTerm.decEq x y, decEqListCTerm xs ys with
+      | isTrue hx, isTrue hxs => isTrue (by rw [hx, hxs])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+
+def decEqListCTypeArg : (xs ys : List CTypeArg) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | x :: xs, y :: ys =>
+      match CTypeArg.decEq x y, decEqListCTypeArg xs ys with
+      | isTrue hx, isTrue hxs => isTrue (by rw [hx, hxs])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+
+def decEqListCtorSpec : (xs ys : List CtorSpec) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | x :: xs, y :: ys =>
+      match CtorSpec.decEq x y, decEqListCtorSpec xs ys with
+      | isTrue hx, isTrue hxs => isTrue (by rw [hx, hxs])
+      | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+      | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+
+def decEqClauses : (xs ys : List (FaceFormula × CTerm)) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | (φ, t) :: xs, (ψ, u) :: ys =>
+      if hφ : φ = ψ then
+        match CTerm.decEq t u, decEqClauses xs ys with
+        | isTrue ht, isTrue hxs => isTrue (by rw [hφ, ht, hxs])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hφ (by cases heq; rfl))
+
+def decEqBranches : (xs ys : List (String × CTerm)) → Decidable (xs = ys)
+  | [], [] => isTrue rfl
+  | [], _ :: _ => isFalse (fun heq => by cases heq)
+  | _ :: _, [] => isFalse (fun heq => by cases heq)
+  | (n, t) :: xs, (n', u) :: ys =>
+      if hn : n = n' then
+        match CTerm.decEq t u, decEqBranches xs ys with
+        | isTrue ht, isTrue hxs => isTrue (by rw [hn, ht, hxs])
+        | isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
+        | _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
+      else isFalse (fun heq => hn (by cases heq; rfl))
+
+end
+
+-- ── Instance declarations ───────────────────────────────────────────────────
+
+instance : DecidableEq CType        := CType.decEq
+instance : DecidableEq CTerm        := CTerm.decEq
+instance : DecidableEq CTypeArg     := CTypeArg.decEq
+instance : DecidableEq CtorSpec     := CtorSpec.decEq
+instance : DecidableEq CTypeSchema  := CTypeSchema.decEq
+
+end CubicalTransport.DecEq
diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean
index f9ad4d7..dbf018a 100644
--- a/CubicalTransport/FFITest.lean
+++ b/CubicalTransport/FFITest.lean
@@ -240,7 +240,37 @@ def tests : List (String × String × String) :=
             { env := .nil, binder := ⟨"i"⟩, body := .interval
             , φ := .top, u := .var "u", t := .var "t" }
         then "yes" else "no"),
-     "yes") ]
+     "yes"),
+    ("Classifier IsFullFace decidable on .top face",
+     (if Question.IsFullFace
+            { env := .nil, binder := ⟨"i"⟩, body := .univ
+            , φ := .top, u := .var "u", t := .var "t" }
+        then "yes" else "no"),
+     "yes"),
+    ("Classifier IsTransport decidable when u = t",
+     (if Question.IsTransport
+            { env := .nil, binder := ⟨"i"⟩, body := .univ
+            , φ := .top, u := .var "x", t := .var "x" }
+        then "yes" else "no"),
+     "yes"),
+    ("Classifier IsTransport rejects when u ≠ t",
+     (if Question.IsTransport
+            { env := .nil, binder := ⟨"i"⟩, body := .univ
+            , φ := .top, u := .var "x", t := .var "y" }
+        then "yes" else "no"),
+     "no"),
+    ("Classifier IsPiLine decidable on .pi body",
+     (if Question.IsPiLine
+            { env := .nil, binder := ⟨"i"⟩, body := .pi .univ .univ
+            , φ := .top, u := .var "u", t := .var "t" }
+        then "yes" else "no"),
+     "yes"),
+    ("Classifier IsIntervalLine rejects on .univ",
+     (if Question.IsIntervalLine
+            { env := .nil, binder := ⟨"i"⟩, body := .univ
+            , φ := .top, u := .var "u", t := .var "t" }
+        then "yes" else "no"),
+     "no") ]
 
 /-- Run every smoke test, print its actual vs expected.  Returns the
     number of failures. -/
diff --git a/CubicalTransport/Face.lean b/CubicalTransport/Face.lean
index 829eca5..d441388 100644
--- a/CubicalTransport/Face.lean
+++ b/CubicalTransport/Face.lean
@@ -22,7 +22,7 @@ inductive FaceFormula where
   | eq1 (i : DimVar)           : FaceFormula  -- (i = 1)
   | meet (ϕ ψ : FaceFormula)  : FaceFormula  -- ϕ ∧ ψ
   | join (ϕ ψ : FaceFormula)  : FaceFormula  -- ϕ ∨ ψ
-  deriving Repr, Inhabited
+  deriving Repr, Inhabited, DecidableEq
 
 -- ── Semantic evaluation ───────────────────────────────────────────────────────
 
diff --git a/CubicalTransport/Interval.lean b/CubicalTransport/Interval.lean
index 61b18cc..459febe 100644
--- a/CubicalTransport/Interval.lean
+++ b/CubicalTransport/Interval.lean
@@ -26,7 +26,7 @@ inductive DimExpr where
   | inv  (r : DimExpr)    : DimExpr    -- 1 − r
   | meet (r s : DimExpr)  : DimExpr    -- r ∧ s
   | join (r s : DimExpr)  : DimExpr    -- r ∨ s
-  deriving Repr, Inhabited
+  deriving Repr, Inhabited, DecidableEq
 
 -- ── Semantic evaluation ───────────────────────────────────────────────────────
 
diff --git a/CubicalTransport/Question.lean b/CubicalTransport/Question.lean
index f4a432e..59fe3be 100644
--- a/CubicalTransport/Question.lean
+++ b/CubicalTransport/Question.lean
@@ -24,6 +24,7 @@
 
 import CubicalTransport.TransportLaws
 import CubicalTransport.CompLaws
+import CubicalTransport.DecEq
 
 namespace Question
 
@@ -138,17 +139,63 @@ def IsIntervalLine (q : CompQ) : Prop :=
 def IsUnivLine (q : CompQ) : Prop :=
   q.body = .univ
 
--- ── Decidability for the syntactic classifiers ───────────────────────────────
--- Only `IsConstLine` is automatically `Decidable` at this layer (it
--- reduces to a Bool equality).  The face- and body-shape classifiers
--- need `DecidableEq FaceFormula` / `DecidableEq CType` from
--- `Topolei.Cubical.DecEq` — registering instances cross-package is
--- left for Level 1.5 once cells-spec / paideia starts dispatching on
--- them.
+-- ── 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);
@@ -163,6 +210,7 @@ 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
@@ -171,6 +219,7 @@ theorem ask_of_full_face (q : CompQ) (h : IsFullFace q) :
 
 /-- 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
@@ -181,6 +230,7 @@ theorem ask_of_empty_face (q : CompQ) (h : IsEmptyFace q) :
     `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) :
@@ -239,6 +289,7 @@ theorem ask_of_stuck (q : CompQ)
     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) :
@@ -248,4 +299,33 @@ theorem ask_of_transport_full_face (q : CompQ)
 
 end CompQ
 
+-- ── Level 2 — automated routing through `simp` ──────────────────────────────
+-- The `@[simp]` attribute on the classifier-conditioned theorems above
+-- lets Lean's `simp` rewrite `q.ask` automatically when a syntactic
+-- classifier hypothesis is in scope.  These examples exercise the
+-- routing on representative shapes; they also serve as sanity checks
+-- that the simp-set composes (none of the lemmas mask each other).
+
+example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
+    let q : CompQ := ⟨env, i, A, .top, u, t⟩
+    q.ask = eval env (u.substDim i .one) := by
+  simp [CompQ.ask_of_full_face, IsFullFace]
+
+example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
+    let q : CompQ := ⟨env, i, A, .bot, u, t⟩
+    q.ask = eval env (.transp i A .bot t) := by
+  simp [CompQ.ask_of_empty_face, IsEmptyFace]
+
+/-- The interval-line question with `u = t` (transport-shaped) and
+    a base that doesn't depend on the binder reduces to `eval env t`.
+    Demonstrates Level 2 chaining: full-face ⊕ transport ⊕ dim-absent
+    base composed automatically by `simp`. -/
+example (env : CEnv) (i : DimVar) (t : CTerm)
+    (hi : t.dimAbsent i = true) :
+    (CompQ.ofTransp env i .interval .top t).ask = eval env t := by
+  apply CompQ.ask_of_transport_full_face
+  · rfl
+  · rfl
+  · exact hi
+
 end Question
diff --git a/CubicalTransport/Syntax.lean b/CubicalTransport/Syntax.lean
index 2eb6a15..043918e 100644
--- a/CubicalTransport/Syntax.lean
+++ b/CubicalTransport/Syntax.lean
@@ -229,6 +229,10 @@ deriving instance Repr for CTypeArg
 deriving instance Repr for CtorSpec
 deriving instance Repr for CTypeSchema
 
+-- DecidableEq for the 5-way mutual block lives in `CubicalTransport.DecEq`
+-- (Lean's `deriving instance DecidableEq` doesn't currently support mutual
+-- inductives — has to be written manually).
+
 -- ── Dimension substitution ────────────────────────────────────────────────────
 -- Substitute dimension variable i with DimExpr r throughout a term.
 --