# Phase 1 History — Transport & Composition Formalization Plan

> **Archival.**  This document is the original implementation plan
> that drove Phase 1 of the cubical-transport HoTT formalization
> (CCHM §5–6).  Every stage listed below is *closed*: see the
> `CubicalTransport/*` modules for the delivered code and
> `CubicalTest.lean` (62/62 passing) for the verification.
>
> Paths in the original plan referred to `Topolei/Cubical/*` from the
> pre-split monolithic repo.  They have been mechanically updated to
> the post-split `CubicalTransport/*` location, but otherwise the
> document is preserved as-is — methodology and step decomposition
> remain useful as a template for future formalization phases (e.g.
> the zigzag port: see `ZIGZAG_PORT.md`).

Stage goal (original): formally verify the CCHM transport and
composition operations in the deep embedding before writing any Rust
— per the project's discipline of stating all external-to-Lean
behavior as Lean axioms before the Rust FFI side is built.

Each step has one clear deliverable, depends only on prior steps,
and can be built and checked independently with `lake build`.

Reference: CCHM §5–6 (Cohen, Coquand, Huber, Mörtberg 2016)

---

## Current state (completed)

| File | Contents |
|------|----------|
| `Interval.lean` | `DimVar`, `DimExpr`, de Morgan laws, `DimExpr.subst`, `eval_subst` |
| `Face.lean` | `FaceFormula`, face laws, `restrict`, `Entails`, endpoint lemmas |
| `Syntax.lean` | `CType`/`CTerm` mutual inductives, `substDim`, `step`, `PathWitness` |
| `Typing.lean` | `HasType` judgment, inversion lemmas, face-boundary connection |

---

## Step 1 — CType dimension substitution

**File:** extend `Syntax.lean` (or new `Syntax/Subst.lean`)

**What:** `CType` needs its own dimension substitution so that a type `A`
can be evaluated at a specific endpoint of the interval.

**Definition:**
```
mutual
  def CType.substDim (i : DimVar) (b : Bool) : CType → CType
    | .univ       => .univ
    | .pi A B     => .pi (A.substDim i b) (B.substDim i b)
    | .path A a t => .path (A.substDim i b)
                           (a.substDimBool i b) (t.substDimBool i b)

  def CTerm.substDimBool (i : DimVar) (b : Bool) : CTerm → CTerm
    -- same as substDim with r = (if b then .one else .zero)
end
```

Note: `CTerm.substDimBool i b` is definitionally
`CTerm.substDim i (if b then .one else .zero)`.
We may define one in terms of the other to avoid duplication.

**Key theorems:**
- `CType.substDim_univ`, `substDim_pi`, `substDim_path` — reduction lemmas
- `CType.substDim_comm` — substituting disjoint dimensions commutes
- `CType.substDim_face` — connection to `FaceFormula.restrict`:
  `(FaceFormula.eq0 i).eval env = true → A.substDim i false = A` (at the face,
  the substitution matches what the face formula asserts)

**Acceptance:** `lake build` with no errors; all three reduction lemmas proved.

---

## Step 2 — DimLine: lines of types

**File:** `CubicalTransport/DimLine.lean`

**What:** A *line of types* `λi. A` — the domain of transport.
Syntactically, it is a pair of a bound dimension variable and a body type.
This is the `A` in `transpⁱ A φ t`.

**Definition:**
```
structure DimLine where
  binder : DimVar
  body   : CType

def DimLine.at0 (L : DimLine) : CType := L.body.substDim L.binder false
def DimLine.at1 (L : DimLine) : CType := L.body.substDim L.binder true
def DimLine.atBool (L : DimLine) (b : Bool) : CType := L.body.substDim L.binder b

def DimLine.const (A : CType) (i : DimVar) : DimLine := { binder := i, body := A }
```

**Key theorems:**
- `DimLine.atBool_false` : `L.atBool false = L.at0`
- `DimLine.atBool_true`  : `L.atBool true  = L.at1`
- `DimLine.const_at0`    : `(DimLine.const A i).at0 = A`
- `DimLine.const_at1`    : `(DimLine.const A i).at1 = A`
  (a constant line has the same type at both endpoints — used in Step 5)
- `DimLine.at_face_zero` — if `(FaceFormula.eq0 L.binder).eval env = true`
  then `L.body.substDim L.binder (env L.binder) = L.at0`
  (the face formula witnesses which endpoint we are at)

**Acceptance:** `lake build`; `const_at0` and `const_at1` proved without sorry.

---

## Step 3 — Extend CTerm with `transp` and `comp`; transport typing rule

**File:** revise `Syntax.lean` and `Typing.lean`

**What:** Add `transp` and `comp` as constructors of `CTerm` now,
so we do not have to reopen the inductive later.
Add the `HasType.transp` rule in `Typing.lean`.

**New CTerm constructors:**
```
| transp (L : DimLine) (φ : FaceFormula) (t : CTerm) : CTerm
  -- transpⁱ (λi.A) φ t

| comp   (L : DimLine) (φ : FaceFormula)
         (u : CTerm)   (t : CTerm)         : CTerm
  -- compⁱ (λi.A) [φ↦u] t
  -- u is the system term; compatibility is enforced in the typing rule
```

**New HasType rule (transport only at this step):**
```
| transp : HasType Γ t L.at0 →
           HasType Γ (.transp L φ t) L.at1
```

`comp` constructor is added to `CTerm` here but its typing rule
is deferred to Step 7, after `System` is defined.

**Also:** update `CTerm.substDim` and `CTerm.substDimBool` to handle
the two new constructors:
```
| .transp L φ t => .transp (L with body := L.body.substDim i b) φ (t.substDimBool i b)
| .comp L φ u t => .comp   (L with body := L.body.substDim i b) φ
                            (u.substDimBool i b) (t.substDimBool i b)
```

**Acceptance:** `lake build`; `HasType.transp` rule present;
existing Syntax/Typing theorems still hold.

---

## Step 4 — Transport identity law

**File:** `CubicalTransport/TransportLaws.lean`

**What:** The fundamental CCHM axiom: transport under the trivial
cofibration `1_F` is the identity.

**Axiom:**
```
axiom transp_id (L : DimLine) (t : CTerm) :
    CTerm.step (.transp L .top t) = t
```

This cannot be proved from the syntax alone — it is a claim about
what the evaluator/kernel must compute. Same pattern as `GPU/Spec.lean`.

**Key theorems derived from `transp_id`:**
- `transp_id_typed` — if `t : L.at0` and we apply `transp_id`,
  then `t : L.at1` (using the fact that `L.at0 = L.at1` when the
  line is constant — from Step 2)
- `transp_const_id` — transport along a constant line is identity
  regardless of `φ`:
  *Proof sketch:* constant line has `at0 = at1 = A`;
  `transp_id` gives the `1_F` case; the general `φ` case
  requires `transp_monotone` (below) or is itself axiomatic.
- `transp_monotone` (axiom or derived):
  if `FaceFormula.Entails φ ψ` then
  `transp L φ t = transp L ψ t` — stronger face → more constrained transport.

**Acceptance:** `transp_id` stated as axiom; `transp_const_id` proved or
stated as axiom with comment explaining which direction is derivable.

---

## Step 5 — Transport–path connection

**File:** `CubicalTransport/TransportLaws.lean` (continued)

**What:** Transport along a constant line recovers path application.
A path `p : Path A a b` is a term that, when transported with `transp`,
moves from `a` to `b`. This step makes that connection explicit.

**Key theorem:**
```
theorem transp_path_apply
    (i : DimVar) (p : CTerm) (A : CType) (a b : CTerm)
    (hp : HasType Γ p (.path A a b)) :
    CTerm.step (.transp (DimLine.const A i) .bot p) =
    CTerm.papp p DimExpr.zero
```
(Transport along a constant line with empty face = path application at 0.
The `1_F` direction gives `b`.)

**Also:**
- `path_as_transp` — states that every path induces a transport:
  `p : Path A a b` gives `transp (const A) _ p : A`
  (the path is itself the transport data)
- `PathWitness_of_transp` — if we have a transport that reduces
  to `a` at `φ = eq0 i` and to `b` at `φ = eq1 i`,
  then there is a `PathWitness` for the abstracted term.
  Connects back to `Syntax.lean`.

**Acceptance:** `transp_path_apply` proved (may use sorry for one
Float/Bool boundary if needed); `PathWitness_of_transp` stated with
proof or clear sorry marking the missing evaluator.

---

## Step 6 — System: partial elements

**File:** `CubicalTransport/System.lean`

**What:** A *system* `[φ↦u]` is a partial term — defined only on
the face where `φ` holds. This is the new concept that composition
requires beyond transport.

**Definition:**
```
structure System where
  face : FaceFormula
  body : CTerm

/-- Compatibility: the system agrees with base term t₀ on the face φ at i=0.
    Formally: whenever φ holds and i=0 holds, body[i:=0] = t₀. -/
def System.CompatAt0 (s : System) (i : DimVar) (t₀ : CTerm) : Prop :=
  ∀ env : DimVar → Bool,
    s.face.eval env = true →
    env i = false →
    s.body.substDimBool i false = t₀
```

**Key theorems:**
- `System.compat_trivial` — the system `[1_F↦u]` is compatible with
  `u[i:=0]` for any `u` (trivial face covers everything)
- `System.compat_bot` — the empty system `[0_F↦u]` is compatible
  with any `t₀` (vacuously true; the face never holds)
- `System.compat_meet` — if `s₁` and `s₂` are both compatible with `t₀`,
  their join system is too (used when combining systems)
- Typing rule for system body:
  ```
  structure System.Typed (Γ : Ctx) (s : System) (L : DimLine) where
    body_typed : HasType Γ s.body L.at1
    -- (body is typed at the *output* end of the line)
  ```

**Acceptance:** `compat_trivial` and `compat_bot` proved without sorry.

---

## Step 7 — Composition declaration + typing rule

**File:** `CubicalTransport/Typing.lean` (extended)

**What:** Add `HasType.comp` — the typing rule for the composition
operation. This is the main event: composition is what makes the
type theory *Kan* (all cubes have fillers).

**New HasType rule:**
```
| comp : HasType Γ t₀ L.at0 →
         System.Typed Γ s L →
         s.CompatAt0 L.binder t₀ →
         HasType Γ (.comp L s.face s.body t₀) L.at1
```

Reading: given a base term `t₀ : L.at0`, a system `[φ↦u]` where
`u : L.at1` on the face `φ`, and a proof that they agree at `i=0`,
the composition `compⁱ (λi.A) [φ↦u] t₀` has type `L.at1`.

**Key theorem:**
```
theorem HasType.comp_inv (h : HasType Γ (.comp L φ u t₀) A) :
    A = L.at1 ∧
    HasType Γ t₀ L.at0 ∧
    ∃ s : System, s.face = φ ∧ s.body = u ∧ System.Typed Γ s L
```
(Inversion: reading off the components of a comp judgment.)

**Acceptance:** `HasType.comp` rule compiles; `comp_inv` proved.

---

## Step 8 — Composition laws

**File:** `CubicalTransport/CompLaws.lean`

**What:** The three fundamental laws of composition. All three are
CCHM axioms — not derivable from the syntax.

**Axioms:**

```
-- Full system: when the face is 1_F, the system fully determines the result.
axiom comp_full (L : DimLine) (u t₀ : CTerm) :
    CTerm.step (.comp L .top u t₀) = u.substDimBool L.binder true

-- Empty system: when the face is 0_F, comp reduces to transport.
axiom comp_empty (L : DimLine) (t₀ : CTerm) :
    CTerm.step (.comp L .bot u t₀) =
    CTerm.step (.transp L .bot t₀)

-- Transport as special case of composition.
-- (This is the definitional reduction in CCHM.)
axiom transp_as_comp (L : DimLine) (φ : FaceFormula) (t₀ : CTerm) :
    CTerm.step (.transp L φ t₀) =
    CTerm.step (.comp L φ t₀ t₀)
    -- system body = constant t₀; compat holds by substDim idempotence
```

**Key derived theorems:**
- `comp_full_typed` — if `HasType.comp` holds with `φ = 1_F`,
  the result equals `u[i:=1]` and has the expected type
- `transp_id_from_comp` — re-derive `transp_id` from `transp_as_comp`
  and `comp_full` (sanity check that the axioms are consistent)
- `comp_absorbs_transp` — if a system already covers the whole face,
  adding a transport does nothing; states the Kan filling property
  informally

**Acceptance:** All three axioms stated; `transp_id_from_comp`
proved as a derived theorem (closes the loop between Steps 4 and 8).

---

## Summary

| Step | File | Deliverable | New sorry? |
|------|------|-------------|------------|
| 1 | `Syntax.lean` extension | `CType.substDim`, reduction lemmas | No |
| 2 | `DimLine.lean` | `DimLine`, endpoint lemmas, `const` | No |
| 3 | `Syntax.lean` + `Typing.lean` | `transp`/`comp` constructors, `HasType.transp` | No |
| 4 | `TransportLaws.lean` | `transp_id` axiom, `transp_const_id` | Axiom (not sorry) |
| 5 | `TransportLaws.lean` | `transp_path_apply`, `PathWitness_of_transp` | Maybe 1 |
| 6 | `System.lean` | `System`, `CompatAt0`, compat lemmas | No |
| 7 | `Typing.lean` | `HasType.comp`, `comp_inv` | No |
| 8 | `CompLaws.lean` | Three comp axioms, `transp_id_from_comp` | Axioms (not sorry) |

The distinction between *axiom* and *sorry* is intentional:
axioms are explicit claims about what the evaluator must satisfy
(same as `GPU/Spec.lean`); sorry marks genuinely incomplete proofs
that need more work.

Once Step 8 is complete, the cubical core is verified up to the
stated axioms, and the Rust FFI implementation of transport/composition
can begin against those as a formal spec — linked back into Lean via
`@[extern]` + `@[implemented_by]` so the kernel can reduce cubical terms
at native speed.