cubical-transport-hott-lean4/docs/PHASE1_HISTORY.md

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.