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

/-
  CubicalTransport.TransportLaws
  =============================
  Residual step-level axioms for transport: subject reduction (T3) and
  path-line shape preservation (T4).

  T1 (`transp_id`) and T2 (`transp_const_id`), formerly stated here as
  step-level axioms, are now NbE theorems in `Cubical/Readback.lean`
  (`readback_transp_id` / `readback_transp_const_id`).  T5 is now
  covered by an eval-level axiom (`eval_transp_face_congr` in
  `Eval.lean`) and its NbE theorem (`readback_transp_face_congr`); the
  step-level form was unused and removed in Stream B #2b.

  The Rust backend's discharge obligations for transport reduce to: the
  eval-level axioms in `Eval.lean`, the readback-level axioms in
  `Readback.lean`, and the two residuals below (T3, T4).

  Why these two residuals stay step-level:
    · T3 / C4 — subject reduction: needs a typing-preservation lemma on
      `eval`/`readback`, which would require a semantic typing relation
      on `CVal` (Stream B #2a, future work).
    · T4 (general case for non-path lines) — vacuous in well-typed code
      (plam at non-path type is a type error), but kept as a syntactic
      fallback.  The path-line case is fully NbE-covered via
      `readback_transp_plam_general` in `Readback.lean` (Stream B #2c).
-/

import CubicalTransport.ValueTyping

-- ── Subject reduction for transport ──────────────────────────────────────────

/-- **T3 (transport subject reduction)** — stepping a well-typed
    transport term preserves the output type.

    **Now a theorem, not an axiom.**  Stage 2.3 (2026-04-23) consolidated
    T3 and C4 into the single `CTerm.step_preserves_type` axiom in
    `ValueTyping.lean`.  T3 here is a direct corollary: the typing rule
    `HasType.transp` places `.transp L.binder L.body φ t` at `L.at1`
    given `t : L.at0`, and `step_preserves_type` propagates that through
    step. -/
theorem transp_step_preserves {ℓ : ULevel}
    (Γ : Ctx) (L : DimLine ℓ) (φ : FaceFormula) (t : CTerm)
    (ht : HasType Γ t L.at0) :
    HasType Γ (CTerm.step (.transp L.binder L.body φ t)) L.at1 :=
  CTerm.step_preserves_type Γ _ _ (HasType.transp L ht)

-- ── Path endpoint typing ──────────────────────────────────────────────────────

/-- Applying a path at 0 gives a term of the path's type. -/
theorem path_zero_typed {ℓ : ULevel} (Γ : Ctx) (p : CTerm) (A : CType ℓ) (a b : CTerm)
    (hp : HasType Γ p (.path A a b)) :
    HasType Γ (.papp p .zero) A :=
  HasType.papp hp

/-- Applying a path at 1 gives a term of the path's type. -/
theorem path_one_typed {ℓ : ULevel} (Γ : Ctx) (p : CTerm) (A : CType ℓ) (a b : CTerm)
    (hp : HasType Γ p (.path A a b)) :
    HasType Γ (.papp p .one) A :=
  HasType.papp hp

-- ── Axiom T4: transport of a plam along a path-typed line (constructive) ─────
--
-- Stage 4.2 tightening (2026-04-23).  The original T4 axiom was
-- non-constructive (`∃ body'`); Rust implementations needed concrete
-- witnesses they couldn't extract.  The replacement is *path-restricted*
-- with an explicit body mirroring `readback_vPathTransp_plam` (the
-- constructive NbE form from Stream B #2c):
--
--   `step (transpⁱ (Path A a b) φ (⟨j⟩ body))`
--     `= ⟨j⟩ (compⁱ A [φ ↦ body, j=0 ↦ a, j=1 ↦ b] body)`
--
-- **Why this is tighter.** Any well-typed `plam j body` has a path type
-- at the line's 0-endpoint (plam introduces only paths).  Transport
-- preserves type, so the line's body must itself be a path type — hence
-- `L.body = .path A a b`.  Non-path lines are vacuous in well-typed
-- code.  Restricting to `.path A a b` loses no generality and gains a
-- concrete Rust discharge.
--
-- **Face-disjointness with the readback NbE form.** Readback's
-- `vPathTransp` arm produces exactly this body on `.plam j body` input
-- (path-input readback), so the axiom and the NbE theorem are consistent.

/-- Axiom T4 (path-restricted, constructive):
    Transport of `⟨j⟩ body` along a line whose body is a path type
    `path A a b` produces `⟨j⟩` of a CCHM-shaped comp witness. -/
theorem transp_plam_is_plam_path {ℓ : ULevel}
    (i : DimVar) (A : CType ℓ) (a b : CTerm)
    (φ : FaceFormula) (j : DimVar) (body : CTerm) :
    CTerm.step (.transp i (.path A a b) φ (.plam j body)) =
    .plam j (.compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body) := by
  -- waits on: FS-H15.
  sorry

-- ── Derived helpers ──────────────────────────────────────────────────────────

/-- The explicit step-reduced body of a path-line-transported plam. -/
def transp_plam_body_path {ℓ : ULevel}
    (i : DimVar) (A : CType ℓ) (a b : CTerm)
    (φ : FaceFormula) (j : DimVar) (body : CTerm) : CTerm :=
  .compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body

-- ── Transport over schema-defined inductive types (REL1) ────────────────────
-- Inductive instances `.ind S params` are neither `.path` nor `.glue`, so
-- transport over them flows through the value-level stuck case in the
-- existing `vTransp_stuck` axiom.  These derived theorems make the API
-- shape explicit for downstream consumers (paideia, topolei).
--
-- A future REL1.1 / REL2 refinement will add pointwise distribution: when
-- the target is a `.ctor S c cParams cArgs`, transport pushes through
-- the args via per-arg-shape rules.  CCHM HIT-transport gives the
-- explicit formula via comp-shaped fillers; for plain inductives the
-- distribution is structurally simpler.

/-- Transport over a non-trivial line in a schema-defined inductive
    `.ind S params` reduces to a stuck `ntransp` neutral.  Derived from
    `eval_transp_nonpath` (`.ind` is not `.path` and not `.glue`) and
    `vTransp_stuck` (`.ind` is not `.pi`). -/
theorem eval_transp_ind {ℓ : ULevel} (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List (Σ ℓ' : ULevel, CType ℓ'))
    (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i (CType.ind (ℓ := ℓ) S params) = false) :
    eval env (.transp i (CType.ind (ℓ := ℓ) S params) φ t) =
    .vneu (.ntransp i (CType.ind (ℓ := ℓ) S params) φ (eval env t)) := by
  rw [eval_transp_nonpath env i (CType.ind (ℓ := ℓ) S params) φ t hφ hA
        (by intro _ _ _ h; nomatch h)
        (by intro _ _ _ _ _ _ _ _ h; nomatch h)]
  exact vTransp_stuck i (CType.ind (ℓ := ℓ) S params) φ (eval env t) hφ hA
    (CType.ind_skeleton_ne_pi S params)

/-- Transport over a constant `.ind` line is the identity (T2 specialised
    to `.ind`).  Direct corollary of `eval_transp_const`. -/
theorem eval_transp_ind_const {ℓ : ULevel} (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List (Σ ℓ' : ULevel, CType ℓ'))
    (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i (CType.ind (ℓ := ℓ) S params) = true) :
    eval env (.transp i (CType.ind (ℓ := ℓ) S params) φ t) = eval env t :=
  eval_transp_const env i (CType.ind (ℓ := ℓ) S params) φ t hφ hA

/-- Transport over `.ind` under a full face is the identity (T1
    specialised to `.ind`). -/
theorem eval_transp_ind_top {ℓ : ULevel} (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List (Σ ℓ' : ULevel, CType ℓ')) (t : CTerm) :
    eval env (.transp i (CType.ind (ℓ := ℓ) S params) .top t) = eval env t :=
  eval_transp_top env i (CType.ind (ℓ := ℓ) S params) t

-- ── Transport over the cubical interval (REL2) ───────────────────────────────
-- `.interval` carries no dim binders (`CType.dimAbsent i .interval = true`
-- for every `i`), so transport on `.interval` is always identity by
-- `eval_transp_const` (or by `eval_transp_top` on the full-face case).

/-- Transport over `.interval` is the identity, regardless of the face
    formula.  Direct corollary of T1 + T2: the interval has no dim
    structure to transport along. -/
theorem eval_transp_interval (env : CEnv) (i : DimVar)
    (φ : FaceFormula) (t : CTerm) :
    eval env (.transp i .interval φ t) = eval env t := by
  by_cases hφ : φ = .top
  · subst hφ; exact eval_transp_top env i .interval t
  · exact eval_transp_const env i .interval φ t hφ rfl

/-- `transp_plam_is_plam_path` restated via the named body. -/
theorem transp_plam_body_path_eq {ℓ : ULevel}
    (i : DimVar) (A : CType ℓ) (a b : CTerm)
    (φ : FaceFormula) (j : DimVar) (body : CTerm) :
    CTerm.step (.transp i (.path A a b) φ (.plam j body)) =
    .plam j (transp_plam_body_path i A a b φ j body) :=
  transp_plam_is_plam_path i A a b φ j body

-- ── Typed transport of a plam on a path-typed line ───────────────────────────

/-- Combines T3 subject reduction with T4 shape preservation on the
    path-typed case: a well-typed `plam`-transport produces a well-typed
    `plam`-witness of the explicit body.

    Parameterised over a DimLine `L` with an explicit `h_path : L.body =
    .path A a b` — lets the caller instantiate against concrete lines
    whether A/a/b vary in `L.binder` or not. -/
theorem transp_plam_step_typed_path {ℓ : ULevel}
    (Γ : Ctx) (L : DimLine ℓ) (A : CType ℓ) (a b : CTerm)
    (h_path : L.body = .path A a b)
    (φ : FaceFormula) (j : DimVar) (body : CTerm)
    (ht : HasType Γ (.plam j body) L.at0) :
    HasType Γ (.plam j (transp_plam_body_path L.binder A a b φ j body))
             L.at1 := by
  have hstep := transp_step_preserves Γ L φ (.plam j body) ht
  -- Rewrite the transport's line-body to the explicit .path form.
  rw [h_path] at hstep
  rwa [transp_plam_body_path_eq] at hstep