/- 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)]