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

/-
  CubicalTransport.Question — The universal question form
  =======================================================
  Implements `docs/QUESTIONS.md` Level 1 (structural reification only).

  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`, …).

  Level 1 commitment: structural reification only.  Existing
  `eval_comp_*` axioms are restated as classifier-conditioned
  `CompQ.Equiv` theorems.  Runtime / soundness behaviour unchanged;
  call sites continue to work via `q.ask`-equality lemmas.

  Levels 2 and 3 (routing through questions, question-driven proofs)
  are deferred — see QUESTIONS.md §4.

  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

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). -/
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. -/
def IsFullFace (q : CompQ) : Prop := q.φ = .top

/-- The face is the empty face — only the base contributes; the
    question reduces to plain transport. -/
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. -/
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 Σ type — Σ reductions apply (REL2.x). -/
def IsSigmaLine (q : CompQ) : Prop :=
  ∃ A B, q.body = .sigma A B

/-- 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 (the interval is dim-absent in itself). -/
def IsIntervalLine (q : CompQ) : Prop :=
  q.body = .interval

/-- The line is the universe — universe-transport reductions apply
    (currently stuck; CCHM univalence-transport via `uaLine`). -/
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.

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

-- ── 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`. -/
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. -/
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). -/
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. -/
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

end Question