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

/-
  CubicalTransport.Inductive
  ==========================
  Helper combinators and canonical schema instances for the REL1
  schema-based inductive (and higher-inductive) type system.

  This module sits *on top of* `Syntax.lean` — it doesn't add new
  primitives, only ergonomic builders.  Every value here is a plain
  CTypeSchema / CType / CTerm; nothing is opaque.  Downstream
  consumers should prefer these helpers over hand-spelling
  CTypeSchema literals so the canonical encodings are maintained
  in one place.

  ## Sections

  · §1  Argument-shape helpers
  · §2  Schema constructors (mkSchema, mkCtor, mkPath)
  · §3  Type-level helpers (CType.list, CType.nat, …, CType.s1, …)
  · §4  Term-level helpers (zeroC, succC, nilC, consC, baseC, loopC, …)
  · §5  Eliminator builders (natElim, listElim, …)

  ## Design notes

  · Boundary clauses inside HIT path constructors reference *dim args*
    via `DimVar.mk "$d_k"` (zero-indexed among `.dim` args) and
    *non-dim args* via `CTerm.var "$arg_k"` (zero-indexed in the full
    arg list).  See INDUCTIVE_TYPES.md §4 for the discipline.

  · The schemas here are concrete values, not `def`s under a
    `noncomputable` veil — `Nat`, `Bool`, etc. are first-class data
    that downstream code can pattern-match on or use as parameters.
-/

import CubicalTransport.Syntax

namespace CubicalTransport.Inductive

-- ── §1. Argument-shape helpers ─────────────────────────────────────────────

/-- A non-recursive argument of a closed CType. -/
@[inline] def argType (A : CType) : CTypeArg := .type A

/-- A reference to the schema's `i`th type parameter. -/
@[inline] def argParam (i : Nat) : CTypeArg := .param i

/-- A recursive argument of the inductive being defined. -/
@[inline] def argSelf : CTypeArg := .self

/-- A dimension argument (path-constructor binder). -/
@[inline] def argDim : CTypeArg := .dim

-- ── §2. Schema constructors ────────────────────────────────────────────────

/-- A point constructor (no boundary system, empty boundary list). -/
@[inline] def mkCtor (name : String) (args : List CTypeArg) : CtorSpec :=
  .mk name args []

/-- A path constructor: a constructor whose argument list contains at
    least one `.dim` arg, and whose boundary system specifies the
    canonical reduction on the corresponding cube faces. -/
@[inline] def mkPath (name : String) (args : List CTypeArg)
    (boundary : List (FaceFormula × CTerm)) : CtorSpec :=
  .mk name args boundary

/-- Build a schema from name, parameter count, and constructor list. -/
@[inline] def mkSchema (name : String) (numParams : Nat)
    (ctors : List CtorSpec) : CTypeSchema :=
  .mk name numParams ctors

-- ── §3. Canonical plain inductive schemas ──────────────────────────────────

/-- The natural numbers as a schema.

    `Nat` has two point constructors:
    - `zero : Nat`
    - `succ : Nat → Nat` (recursive arg: `.self`)
-/
def natSchema : CTypeSchema :=
  mkSchema "Nat" 0
    [ mkCtor "zero" []
    , mkCtor "succ" [.self] ]

/-- The booleans as a schema. -/
def boolSchema : CTypeSchema :=
  mkSchema "Bool" 0
    [ mkCtor "false" []
    , mkCtor "true"  [] ]

/-- Polymorphic lists as a schema, parameterised by the element type. -/
def listSchema : CTypeSchema :=
  mkSchema "List" 1
    [ mkCtor "nil"  []
    , mkCtor "cons" [.param 0, .self] ]

-- ── §4. Canonical HIT schemas ──────────────────────────────────────────────

/-- The circle `S¹` as a HIT.

    Constructors:
    - `base : S¹`                       (point)
    - `loop : (i : I) → S¹`             (path: `loop @ 0 = base = loop @ 1`)

    Boundary: at `i=0` and `i=1`, `loop` returns `base`.

    The `loop` boundary references `base` via the schema's own
    `.ctor` constructor at the same schema (recursive self-reference
    inside the schema's body).  We construct it inline here. -/
def s1Schema : CTypeSchema :=
  -- Build a self-referential schema: `loop`'s boundary uses
  -- `.ctor s1Schema "base" [] []` which in turn references `s1Schema`.
  -- Since the recursion is structural through the schema's data
  -- (not through a Lean-level fixpoint), we define `s1Schema` via
  -- Lean's well-founded recursion through structural data; the
  -- result is a finite, well-formed `CTypeSchema` value — but Lean
  -- won't accept a literal self-recursive `def` like this.
  --
  -- Workaround: take the schema *name* + a fresh local schema that
  -- refers to itself via a placeholder.  At construction time we
  -- patch the placeholder.  This is implemented as a small fix-up
  -- below.
  let baseAt (s : CTypeSchema) : CTerm := .ctor s "base" [] []
  -- We need `s1Schema = mkSchema "S¹" 0 [base, loop]` where
  -- `loop` carries a boundary that references `s1Schema`.
  -- Lean's `let rec` doesn't handle this for `CTypeSchema` the
  -- way it would for a function — but we can use a `where`-style
  -- two-step build: first build a "stub" schema, then build the
  -- final `loop` referring to it.  Both schemas have the same
  -- structural shape, so `s1Schema` is well-defined.
  let stub : CTypeSchema :=
    mkSchema "S¹" 0
      [ mkCtor "base" []
      , mkPath "loop" [.dim] [] ]
  let d : DimVar := ⟨"$d_0"⟩
  mkSchema "S¹" 0
    [ mkCtor "base" []
    , mkPath "loop" [.dim]
        [ (.eq0 d, baseAt stub)
        , (.eq1 d, baseAt stub) ] ]

/-- The interval as a HIT.

    Constructors:
    - `zero : I`
    - `one  : I`
    - `seg  : (i : I) → I` with `seg @ 0 = zero`, `seg @ 1 = one`. -/
def intervalSchema : CTypeSchema :=
  let stub : CTypeSchema :=
    mkSchema "I" 0
      [ mkCtor "zero" []
      , mkCtor "one"  []
      , mkPath "seg" [.dim] [] ]
  let zeroAt (s : CTypeSchema) : CTerm := .ctor s "zero" [] []
  let oneAt  (s : CTypeSchema) : CTerm := .ctor s "one"  [] []
  let d : DimVar := ⟨"$d_0"⟩
  mkSchema "I" 0
    [ mkCtor "zero" []
    , mkCtor "one"  []
    , mkPath "seg" [.dim]
        [ (.eq0 d, zeroAt stub)
        , (.eq1 d, oneAt  stub) ] ]

/-- Propositional truncation `‖A‖₋₁` as a HIT.

    Constructors:
    - `inT  : A → ‖A‖₋₁`           (point)
    - `squash : (x y : ‖A‖₋₁) → (i : I) → ‖A‖₋₁`
        with `squash x y @ 0 = x`, `squash x y @ 1 = y`. -/
def propTruncSchema : CTypeSchema :=
  let d : DimVar := ⟨"$d_0"⟩
  -- arg index: 0 = first .self ("$arg_0"), 1 = second .self ("$arg_1"),
  -- 2 = .dim ($d_0).  Boundary references positional arg names.
  mkSchema "‖_‖₋₁" 1
    [ mkCtor "inT"    [.param 0]
    , mkPath "squash" [.self, .self, .dim]
        [ (.eq0 d, .var "$arg_0")
        , (.eq1 d, .var "$arg_1") ] ]

-- ── §5. Type-level helpers ─────────────────────────────────────────────────

/-- The `CType` for natural numbers. -/
@[inline] def CType.natC : CType := .ind natSchema []

/-- The `CType` for booleans. -/
@[inline] def CType.boolC : CType := .ind boolSchema []

/-- The `CType` for lists with element type `A`. -/
@[inline] def CType.listC (A : CType) : CType := .ind listSchema [A]

/-- The `CType` for the circle. -/
@[inline] def CType.s1C : CType := .ind s1Schema []

/-- The `CType` for the interval. -/
@[inline] def CType.intervalC : CType := .ind intervalSchema []

/-- The `CType` for propositional truncation `‖A‖₋₁`. -/
@[inline] def CType.propTruncC (A : CType) : CType :=
  .ind propTruncSchema [A]

-- ── §6. Term-level helpers ─────────────────────────────────────────────────

namespace CTerm

/-- The `CTerm` `zero : Nat`. -/
@[inline] def zeroC : CTerm := .ctor natSchema "zero" [] []

/-- The `CTerm` `succ n` for a given `n : Nat`. -/
@[inline] def succC (n : CTerm) : CTerm := .ctor natSchema "succ" [] [n]

/-- The `CTerm` `false : Bool`. -/
@[inline] def falseC : CTerm := .ctor boolSchema "false" [] []

/-- The `CTerm` `true : Bool`. -/
@[inline] def trueC  : CTerm := .ctor boolSchema "true"  [] []

/-- The `CTerm` `nil : List A`.  Carries the element type as parameter. -/
@[inline] def nilC (A : CType) : CTerm := .ctor listSchema "nil" [A] []

/-- The `CTerm` `cons x xs : List A`. -/
@[inline] def consC (A : CType) (x xs : CTerm) : CTerm :=
  .ctor listSchema "cons" [A] [x, xs]

/-- The `CTerm` `base : S¹`. -/
@[inline] def baseC : CTerm := .ctor s1Schema "base" [] []

/-- The `CTerm` `loop @ r : S¹` where `r : DimExpr`. -/
@[inline] def loopC (r : DimExpr) : CTerm :=
  .ctor s1Schema "loop" [] [.dimExpr r]

/-- The `CTerm` `inT a : ‖A‖₋₁`. -/
@[inline] def inTC (A : CType) (a : CTerm) : CTerm :=
  .ctor propTruncSchema "inT" [A] [a]

/-- The `CTerm` `squash x y @ r : ‖A‖₋₁`. -/
@[inline] def squashC (A : CType) (x y : CTerm) (r : DimExpr) : CTerm :=
  .ctor propTruncSchema "squash" [A] [x, y, .dimExpr r]

/-- Build a Nat literal `n` as a tower of `succ`s on `zero`. -/
def natLit : Nat → CTerm
  | 0     => zeroC
  | n + 1 => succC (natLit n)

end CTerm

-- ── §7. Eliminator builders ────────────────────────────────────────────────

/-- Build an `indElim` for `Nat`.  `motive` is the result type-former,
    `caseZero` the body for `zero`, `caseSucc` the body for `succ`
    (curried as `λ pred ih. body`).  `target` is the natural being
    eliminated. -/
def natElim (motive caseZero caseSucc target : CTerm) : CTerm :=
  .indElim natSchema [] motive
    [("zero", caseZero), ("succ", caseSucc)] target

/-- Build an `indElim` for `Bool`. -/
def boolElim (motive caseFalse caseTrue target : CTerm) : CTerm :=
  .indElim boolSchema [] motive
    [("false", caseFalse), ("true", caseTrue)] target

/-- Build an `indElim` for `List A`.  `caseCons` is curried as
    `λ head tail ih. body`. -/
def listElim (A : CType) (motive caseNil caseCons target : CTerm) : CTerm :=
  .indElim listSchema [A] motive
    [("nil", caseNil), ("cons", caseCons)] target

end CubicalTransport.Inductive