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

/-
  Topolei.Cubical.Line
  ====================
  DimLine extensions: reversal and concatenation (cells-spec §14,
  `transp_concat` Critical obligation).

  `DimLine` itself is defined in `Cubical/DimLine.lean` as
  `{ binder : DimVar, body : CType }`.  This module adds the two
  line-level operations that cell composition depends on (cells-spec
  §6.2 `Cell.seq` / `Cell.inv`):

  - **`DimLine.inv`** — reversed line (endpoint swap).  Implemented via
    `substDimExpr` with `.inv (.var binder)`.  The endpoint lemmas are
    *Lean-discharge* axioms: their proofs require a `DimExpr` normaliser
    that reduces `.inv .zero` to `.one` (and `.inv .one` to `.zero`),
    which the current substitution pass does not perform.  When a
    `DimExpr.normalize` function lands, these will become theorems.

  - **`DimLine.concat`** — line concatenation (CCHM universe-hcomp
    construction, cells-spec §5.6).  Because topolei does not currently
    have a universe-level hcomp CType former, `concat` is stated as a
    *Rust-discharge* axiom: the backend must synthesise the concatenated
    line type via the universe-hcomp construction.

  - **`transp_concat`** (cells-spec §14 Critical) — transport along a
    concatenated line factors as the sequential composition of
    transports.  Stated at the value level via `vTranspLine`, and
    lifted to the spec theorem.  Rust-discharge.

  Discipline on axiom provenance
  -------------------------------
  We distinguish two kinds of axiom:

  - *Rust-discharge* — the axiom encodes a reduction rule that the Rust
    cubical evaluator will implement.  `concat`, its endpoint lemmas,
    and `vTranspLine_concat` are of this kind: they state how universe
    hcomp evaluates, which is a backend responsibility.

  - *Lean-discharge* — the axiom encodes a property that a later Lean
    module will prove.  `DimLine.inv_at0` / `inv_at1` are of this kind:
    once `DimExpr.normalize` exists in Lean, they become theorems
    without Rust involvement.

  Both are legitimate spec obligations; the provenance tag tells you
  *where* the obligation is discharged.
-/

import CubicalTransport.Transport

-- ── DimLine.inv ──────────────────────────────────────────────────────────────
-- Reversed line via DimExpr substitution.  `.inv (.var i)` flips the
-- dimension: at i = 0 it evaluates to 1, at i = 1 to 0.  After the outer
-- Bool-endpoint substitution, the line has swapped endpoints.

/-- Line reversal.  The reversed line exchanges the two endpoints:
    `(inv L).at0 = L.at1` and `(inv L).at1 = L.at0` (see the axioms
    below for the semantic justification pending `DimExpr.normalize`). -/
def DimLine.inv (L : DimLine) : DimLine :=
  { binder := L.binder
    body   := L.body.substDimExpr L.binder (.inv (.var L.binder)) }

/-- At dim 0, the reversed line has the original at-1 endpoint.

    **Lean-discharge obligation.**  Proof requires a `DimExpr.normalize`
    function recognising `.inv .zero = .one` syntactically.  The naive
    substitution `((.var i).substDim i .zero = .zero` composed with
    `.inv ·` produces `.inv .zero`, not the reduced `.one` — so the
    endpoint equality is not `rfl` at the raw substitution layer.
    Becomes a theorem once normalization is added. -/
axiom DimLine.inv_at0 (L : DimLine) : (DimLine.inv L).at0 = L.at1

/-- At dim 1, the reversed line has the original at-0 endpoint.
    **Lean-discharge obligation** (see `inv_at0`). -/
axiom DimLine.inv_at1 (L : DimLine) : (DimLine.inv L).at1 = L.at0

/-- Double reversal is the original line.  Depends on the DimExpr
    normalisation `.inv (.inv r) = r`.  **Lean-discharge obligation.** -/
axiom DimLine.inv_inv (L : DimLine) : DimLine.inv (DimLine.inv L) = L

-- ── DimLine.concat ──────────────────────────────────────────────────────────
-- Line concatenation via universe hcomp (CCHM §6.2, cells-spec §5.6).
-- `CType` has no universe-hcomp former yet, so the operation is stated
-- axiomatically.  The backend will synthesise the concatenated line
-- via `hcomp` in the universe.

/-- Line concatenation.  Given `L : A → B` and `M : B → C` (matched by
    the hypothesis `L.at1 = M.at0`), produces a line from `A` to `C`.

    **Rust-discharge axiom.**  The CCHM construction is
    `(L · M)(i) = hcomp^j U [i=0 ↦ L(~j), i=1 ↦ M(j)] B` (universe
    hcomp filling the square whose top is `L` and whose right is `M`).
    The backend implements this; here we carry the structural
    operation without a concrete CType body. -/
axiom DimLine.concat (L M : DimLine) (h : L.at1 = M.at0) : DimLine

/-- The concatenated line retains the left line's input endpoint. -/
axiom DimLine.concat_at0 (L M : DimLine) (h : L.at1 = M.at0) :
    (DimLine.concat L M h).at0 = L.at0

/-- The concatenated line exposes the right line's output endpoint. -/
axiom DimLine.concat_at1 (L M : DimLine) (h : L.at1 = M.at0) :
    (DimLine.concat L M h).at1 = M.at1

-- ── transp_concat (cells-spec §14 Critical) ─────────────────────────────────
-- Transport along a concatenation equals the composition of transports
-- along the two factors.  Stated at the value level via `vTranspLine`,
-- at the empty face `.bot` (generic transport; T1 covers the full-face
-- case trivially).

/-- **Rust-discharge axiom** underlying `transp_concat`.  The universe-
    hcomp construction for `concat` reduces, under `vTranspLine`, to the
    sequential application of transports along the two factor lines.

    Consistency with existing axioms:
    · If `L` is constant (T2-reducible), `vTranspLine L .bot v = v`, so
      the RHS collapses to `vTranspLine M .bot v` — matching the fact
      that `concat (const A) M = M` up to endpoint alignment (a
      separate unit law, stated in Phase 2 Cell/Compose.lean).
    · If both are constant, both sides reduce to `v` via T2.
    · On general lines the RHS is the CCHM sequential-transport form,
      which is exactly what universe hcomp computes. -/
axiom vTranspLine_concat
    (L M : DimLine) (h : L.at1 = M.at0) (v : CVal) :
    vTranspLine (DimLine.concat L M h) .bot v =
    vTranspLine M .bot (vTranspLine L .bot v)

/-- **`transp_concat` (cells-spec §14 Critical).**  Transport along a
    concatenation is the composition of transports.  Restatement of
    `vTranspLine_concat` at the spec theorem level.

    This is the computational backbone of `Cell.seq` associativity
    (cells-spec §6.2) and of the groupoid laws on cells (cells-spec
    §1.3): monad laws on cells reduce to groupoid laws on paths, and
    path concatenation's transport law is `transp_concat`. -/
theorem transp_concat
    (L M : DimLine) (h : L.at1 = M.at0) (v : CVal) :
    vTranspLine (DimLine.concat L M h) .bot v =
    vTranspLine M .bot (vTranspLine L .bot v) :=
  vTranspLine_concat L M h v

-- ── Constant-line specialisations ───────────────────────────────────────────
-- Two corollaries that Phase 2 Cell/Compose.lean will consume when
-- proving cell_left_unit / cell_right_unit on the nose.

/-- Transport along `(const A i) · L` equals transport along `L` alone
    (provided the `const A i` is truly constant, i.e. `i ∉ A`).

    Combines `vTranspLine_concat` with T2 (`vTransp_const`) on the
    constant left factor. -/
theorem transp_concat_const_left
    (A : CType) (i : DimVar) (L : DimLine)
    (hA : CType.dimAbsent i A = true)
    (h  : (DimLine.const A i).at1 = L.at0) (v : CVal) :
    vTranspLine (DimLine.concat (DimLine.const A i) L h) .bot v =
    vTranspLine L .bot v := by
  rw [vTranspLine_concat (DimLine.const A i) L h v]
  rw [vTranspLine_const (DimLine.const A i) .bot v (by
    -- DimLine.const A i has body = A and binder = i; dimAbsent reduces.
    show CType.dimAbsent i A = true; exact hA)]

/-- Transport along `L · (const C i)` equals transport along `L` alone
    (provided the `const C i` is truly constant).

    Combines `vTranspLine_concat` with T2 on the constant right factor. -/
theorem transp_concat_const_right
    (L : DimLine) (C : CType) (i : DimVar)
    (hC : CType.dimAbsent i C = true)
    (h  : L.at1 = (DimLine.const C i).at0) (v : CVal) :
    vTranspLine (DimLine.concat L (DimLine.const C i) h) .bot v =
    vTranspLine L .bot v := by
  rw [vTranspLine_concat L (DimLine.const C i) h v]
  rw [vTranspLine_const (DimLine.const C i) .bot _ (by
    show CType.dimAbsent i C = true; exact hC)]