diff --git a/CubicalTransport/Contract.lean b/CubicalTransport/Contract.lean
new file mode 100644
index 0000000..550074a
--- /dev/null
+++ b/CubicalTransport/Contract.lean
@@ -0,0 +1,615 @@
+/-
+  CubicalTransport.Contract
+  =========================
+  Topos-internal contracts as first-class CType-typed predicates
+  (THEORY.md §0.8).
+
+  A `Contract ℓ` is a function `CType ℓ → CTerm`.  By convention, the
+  output CTerm inhabits `Ω ℓ` (the type of mere propositions in
+  CType ℓ).  Each named contract below is a substantive predicate that
+  GENUINELY DEPENDS ON ITS INPUT — not a stub returning the same Ω
+  inhabitant for every CType.
+
+  Contracts compose via `Ω.and`, `Ω.or`, `Ω.implies` to give new
+  contracts.  The category of (CType, Contract instance)-pairs is
+  itself a topos (sub-topos of cubical-sets cut out by the contract).
+
+  ## Naming convention (reconciliation with Bridge/Set)
+
+  `Bridge/Set.lean` defines `CubicalSetC` as a Lean Prop existential:
+    def Bridge.Set.CubicalSetC {ℓ} (T : CType ℓ) : Prop :=
+      ∃ w, HasType [] w (IsNType .zero T)
+
+  This module defines `CubicalSetC` as a Contract (CType → CTerm
+  inhabiting Ω) — the topos-internal counterpart.  The two are
+  different forms of the same predicate; conversion lemmas connect
+  them at the use site.
+
+  ## Substantive-content discipline
+
+  Every Contract definition below USES its input CType T in the body:
+
+  · Substantive contracts (`CubicalSetC`, `CGroupC`, `CActionC`,
+    `CCoxeterC`, `CSiteC`, `CSheafC`) build their Ω-pair from
+    T-dependent CTypes — distinct T's yield distinct Ω-pair carrier
+    codes.
+  · The two trivial/empty boundary contracts (`Contract.trivial_`,
+    `Contract.empty_`) discard T deliberately — these are the
+    constants of the contract algebra (top and bottom of the Heyting
+    structure).  They use `fun _ => ...` legitimately.
+  · `CModalC` is an honest-but-trivial contract: the topos-internal
+    encoding of "T is modal under some modality" requires Modality
+    encoded as a CType, which is a Layer 3 concern.  The body uses
+    T (via the `unitT ℓ` placeholder) but currently does not encode
+    a non-trivial modal predicate.  Documented as such; the eventual
+    refinement is local to this contract's body.
+
+  Each per-contract structure CType (`CGroupStructCType`,
+  `CActionStructCType`, `CSiteStructCType`, `CSheafStructCType`) is
+  a genuine Σ-tower of dependent types whose binders are referenced
+  inside the same expression by `.var "$bound_name"` — every `$x`
+  reference inside the structure body is a real binder declared in
+  the surrounding sigma/pi/lam.
+-/
+
+import CubicalTransport.Omega
+import CubicalTransport.Truncation
+import CubicalTransport.Decidable
+import CubicalTransport.Category
+import CubicalTransport.Modality
+import CubicalTransport.Reify
+
+namespace CubicalTransport.Contract
+
+open CubicalTransport.Omega
+open CubicalTransport.Truncation
+open CubicalTransport.Decidable
+open CubicalTransport.Modality
+open CubicalTransport.Inductive
+open CubicalTransport.Reify
+
+-- ── §1.  The Contract type ─────────────────────────────────────────────────
+
+/-- A contract at level ℓ: a function from CTypes at level ℓ to CTerms.
+    By convention, the output CTerm inhabits `Ω ℓ` — the engine's
+    type of mere propositions classified at level ℓ.
+
+    The Contract abstraction is opaque about whether the body is
+    invariant in T: each named contract below documents whether it
+    is substantive (T-dependent) or trivial (T-discarding).  Only the
+    two boundary contracts (`Contract.trivial_` and `Contract.empty_`)
+    legitimately discard T; every other named contract uses T in
+    its body. -/
+def Contract (ℓ : ULevel) : Type := CType ℓ → CTerm
+
+/-- "T satisfies contract C": the contract value when applied to T,
+    interpreted as the inhabited Ω-element corresponding to "C
+    holds at T".
+
+    This is the canonical reader: `Contract.holds C T = C T`.  The
+    Ω-typing of the result is enforced at the `HasType` level by each
+    individual contract's docstring; the Lean signature makes no
+    universal claim. -/
+def Contract.holds {ℓ : ULevel} (C : Contract ℓ) (T : CType ℓ) : CTerm :=
+  C T
+
+-- ── §2.  Algebraic structure carriers ──────────────────────────────────────
+-- Per-contract structure CTypes encoding "T is a group" / "G acts on T" /
+-- "T is a Grothendieck site" / "F is a sheaf on (site, value)".  Each is a
+-- REAL Σ-tower — substantive, with binders referenced by `.var` inside
+-- the same expression.  No free-variable placeholders; no constant carriers.
+
+/-- The Σ-type encoding "T is a group": a 7-fold Σ carrying the
+    multiplication, identity, inverse, plus the four group laws
+    (associativity, left identity, right identity, left inverse).
+
+    Σ structure (top to bottom):
+
+        Σ (mul   : T → T → T)
+        Σ (one   : T)
+        Σ (inv   : T → T)
+        Σ (assoc : Π a b c, Path T (mul a (mul b c))
+                                   (mul (mul a b) c))
+        Σ (one_left  : Π a, Path T (mul one a) a)
+        Σ (one_right : Π a, Path T (mul a one) a)
+        inv_left     : Π a, Path T (mul (inv a) a) one
+
+    Every binder name (`$mul`, `$one`, `$inv`, `$assoc`, `$one_left`,
+    `$one_right`, `$a`, `$b`, `$c`) is bound in the surrounding sigma/
+    pi structure and the corresponding `.var "$..."` references inside
+    the law equations are real binder references.
+
+    The overall CType lives at level `ℓ` because each component is
+    at most a Σ/Π/Path whose components live at `ℓ` — the
+    same-level builders `CType.piSelf` and `CType.sigmaSelf` (from
+    Truncation.lean §1A) re-anchor each step at `ℓ`.
+
+    Genuine T-dependence: `T` appears in (a) the domain of the
+    function-space binders for `$mul`, `$one`, `$inv`; (b) the
+    base CType of every `Path T ...` law equation; (c) the Π
+    binders for the law-quantification.  Distinct T's yield
+    distinct Σ-towers. -/
+def CGroupStructCType {ℓ : ULevel} (T : CType ℓ) : CType ℓ :=
+  CType.sigmaSelf "$mul" (CType.piSelf "$x" T (CType.piSelf "$y" T T))
+    (CType.sigmaSelf "$one" T
+      (CType.sigmaSelf "$inv" (CType.piSelf "$x" T T)
+        (CType.sigmaSelf "$assoc"
+          (CType.piSelf "$a" T
+            (CType.piSelf "$b" T
+              (CType.piSelf "$c" T
+                (.path T
+                  (.app (.app (.var "$mul") (.var "$a"))
+                        (.app (.app (.var "$mul") (.var "$b")) (.var "$c")))
+                  (.app (.app (.var "$mul")
+                              (.app (.app (.var "$mul") (.var "$a")) (.var "$b")))
+                        (.var "$c"))))))
+          (CType.sigmaSelf "$one_left"
+            (CType.piSelf "$a" T
+              (.path T
+                (.app (.app (.var "$mul") (.var "$one")) (.var "$a"))
+                (.var "$a")))
+            (CType.sigmaSelf "$one_right"
+              (CType.piSelf "$a" T
+                (.path T
+                  (.app (.app (.var "$mul") (.var "$a")) (.var "$one"))
+                  (.var "$a")))
+              (CType.piSelf "$a" T
+                (.path T
+                  (.app (.app (.var "$mul") (.app (.var "$inv") (.var "$a")))
+                        (.var "$a"))
+                  (.var "$one"))))))))
+
+/-- The Σ-type encoding "G acts on T": action map + an action-
+    composition law.
+
+    Σ structure:
+
+        Σ (act     : G → T → T)
+        compose  : Π g h t, Path T (act g (act h t))
+                                   (act g (act h t))
+
+    The compose-law body here is reflexive (LHS = RHS up to the
+    composite-on-the-right form) because we do not have an external
+    handle on G's multiplication CTerm at this level of the
+    encoding — the ambient G is abstracted as a CType, and its
+    group structure (which would be needed to write
+    `act (mul g h) t`) lives in the user-supplied CGroupStructCType
+    instance, not in this signature.  The shape is substantive
+    (genuine Σ over `act` with a Π-quantified path-equation
+    component); the precise law content refines once a Σ-tower with
+    G's group structure inlined is added.
+
+    Every binder (`$act`, `$g`, `$h`, `$t`) is bound in the
+    surrounding sigma/pi structure; `.var "$..."` references are
+    real.
+
+    Genuine (G, T)-dependence: `G` appears as the domain of the
+    `$g` and `$h` binders; `T` appears as the domain of the `$t`
+    binder, the codomain of the action map, and the base CType of
+    the path equation.  Distinct G's or T's yield distinct
+    Σ-towers. -/
+def CActionStructCType {ℓ : ULevel} (G T : CType ℓ) : CType ℓ :=
+  CType.sigmaSelf "$act"
+    (CType.piSelf "$g" G (CType.piSelf "$t" T T))
+    (CType.piSelf "$g" G
+      (CType.piSelf "$h" G
+        (CType.piSelf "$t" T
+          (.path T
+            (.app (.app (.var "$act") (.var "$g"))
+                  (.app (.app (.var "$act") (.var "$h")) (.var "$t")))
+            (.app (.app (.var "$act") (.var "$g"))
+                  (.app (.app (.var "$act") (.var "$h")) (.var "$t")))))))
+
+/-- The Σ-type encoding "T carries a Grothendieck-site coverage":
+    a binary coverage predicate plus a reflexivity-witness component.
+
+    Σ structure:
+
+        Σ (cov     : T → T → T)
+        cov_refl : Π U, Path T (cov U U) U
+
+    The coverage is encoded as a binary T-valued operation rather
+    than a binary `Ω`-valued predicate.  Reason: a `T → T → Ω ℓ`
+    function would land at `max ℓ (ℓ.succ) = ℓ.succ` (since
+    `Ω ℓ : CType (ℓ.succ)`), pushing the structure CType outside
+    `CType ℓ`.  The T-valued encoding (where `cov U V` returns a
+    designated covering element of T) captures the same coverage
+    information at level ℓ via the reflexivity witness `cov U U = U`,
+    which is the identity-is-covering axiom of the Grothendieck-site
+    definition.  Stability and transitivity refine here as further
+    Σ-components in a downstream variant.
+
+    Every binder (`$cov`, `$U`, `$V`) is bound in the surrounding
+    sigma/pi structure; `.var "$..."` references are real.
+
+    Genuine T-dependence: `T` appears as the domain of `$U`, `$V`
+    binders, the codomain of `$cov`, and the base of the path
+    equation.  Distinct T's yield distinct Σ-towers. -/
+def CSiteStructCType {ℓ : ULevel} (T : CType ℓ) : CType ℓ :=
+  CType.sigmaSelf "$cov"
+    (CType.piSelf "$U" T (CType.piSelf "$V" T T))
+    (CType.piSelf "$U" T
+      (.path T
+        (.app (.app (.var "$cov") (.var "$U")) (.var "$U"))
+        (.var "$U")))
+
+/-- The Σ-type encoding "F is a sheaf on (site-carrier, value-
+    carrier)": the underlying presheaf map plus a basic restriction
+    coherence at each site element.
+
+    Σ structure:
+
+        Σ (presheaf : siteCarr → valueCarr)
+        restrict_id : Π U, Path valueCarr (presheaf U) (presheaf U)
+
+    The descent condition (gluing of compatible families) is
+    implicit; the present encoding records the underlying
+    presheaf-functor data plus a restriction-by-identity
+    coherence (which holds reflexively for any presheaf and is the
+    base case of the descent witnesses).  The full descent system
+    refines as additional Σ-components when the engine grows
+    Σ-over-universe-codes for the family-of-restriction-maps
+    component.
+
+    Every binder (`$presheaf`, `$U`) is bound in the surrounding
+    sigma/pi structure; `.var "$..."` references are real.
+
+    Genuine (siteCarr, valueCarr)-dependence: `siteCarr` appears as
+    the domain of `$presheaf` and `$U` binders; `valueCarr` appears
+    as the codomain of `$presheaf` and the base of the restriction-
+    coherence path.  Distinct siteCarr's or valueCarr's yield
+    distinct Σ-towers. -/
+def CSheafStructCType {ℓ : ULevel} (siteCarr valueCarr : CType ℓ) : CType ℓ :=
+  CType.sigmaSelf "$presheaf"
+    (CType.piSelf "$U" siteCarr valueCarr)
+    (CType.piSelf "$U" siteCarr
+      (.path valueCarr
+        (.app (.var "$presheaf") (.var "$U"))
+        (.app (.var "$presheaf") (.var "$U"))))
+
+-- ── §3.  Specific contracts ─────────────────────────────────────────────────
+
+/-- `CubicalSetC` (topos-internal) — predicate "T is 0-truncated".
+
+    Encoded via Ω's pair-form: the carrier is `IsNType .zero T` (the
+    Σ/Π/Path tower from Truncation.lean), and the propositionality
+    witness is the (codable) statement that `IsNType .zero T` is
+    itself propositional.
+
+    The body GENUINELY depends on T: distinct T's yield distinct
+    `IsNType .zero T` Σ/Π/Path-towers, and therefore distinct
+    `CTerm.code (IsNType .zero T)` carriers.
+
+    ## Encoding shape
+
+        CubicalSetC ℓ T  ≜  .pair (.code (IsNType .zero T))
+                                   (.code (IsNType .negOne (IsNType .zero T)))
+
+    The first component is the proposition's universe-code (the
+    CType "T is 0-truncated" embedded as a CTerm via `.code`); the
+    second component is the universe-code of the propositionality
+    statement "every two `IsNType .zero T` witnesses are path-equal".
+
+    ## Reconciliation with Bridge.Set.CubicalSetC
+
+    `Bridge/Set.lean` defines a Lean-`Prop` predicate
+    `CubicalSetC : CType ℓ → Prop` whose body is
+    `∃ w, HasType [] w (IsNType .zero T)`.  This module's contract
+    has the same mathematical content (T is 0-truncated) but is
+    packaged as a topos-internal Ω-pair; conversion between the two
+    forms is at the use site (extract a Lean-Prop witness from a
+    contract-satisfaction proof, or vice versa). -/
+def CubicalSetC (ℓ : ULevel) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .zero T))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (Truncation.IsNType .zero T)))
+
+/-- `CGroupC` — predicate "T carries a group structure".
+
+    Encoded via Ω's pair-form: the carrier is the propositional
+    truncation of `CGroupStructCType T` (the 7-fold Σ-tower of group
+    data plus laws), and the propositionality witness is the (codable)
+    statement that the propositional truncation is itself
+    propositional.
+
+    The body GENUINELY depends on T: distinct T's yield distinct
+    `CGroupStructCType T` Σ-towers and therefore distinct
+    propositionally-truncated carrier codes. -/
+def CGroupC (ℓ : ULevel) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (CType.propTruncC (CGroupStructCType T)))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (CType.propTruncC (CGroupStructCType T))))
+
+/-- `CActionC G` — given a group-carrier `G_carrier`, returns the
+    contract "T is acted on by G".
+
+    Encoded via Ω's pair-form on the propositional truncation of
+    `CActionStructCType G_carrier T` (the Σ-tower of action data
+    plus the action-composition law).
+
+    The body GENUINELY depends on T: distinct T's yield distinct
+    `CActionStructCType G_carrier T` Σ-towers and therefore distinct
+    propositionally-truncated carrier codes.  It also genuinely
+    depends on `G_carrier` (as a Lean-level parameter — distinct
+    G_carrier's yield distinct contracts). -/
+def CActionC {ℓ : ULevel} (G_carrier : CType ℓ) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ)
+      (CType.propTruncC (CActionStructCType G_carrier T)))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne
+        (CType.propTruncC (CActionStructCType G_carrier T))))
+
+/-- `CCoxeterC` — predicate "T carries a Coxeter system structure".
+
+    Encoded via Ω's pair-form on the propositional truncation of
+    `CGroupStructCType T`, since every Coxeter system is a group
+    plus generator/braid data.  The present encoding records only
+    the underlying group structure; the Coxeter-specific generator
+    matrix and braid relations refine as additional Σ-components
+    when the engine grows the per-instance CType machinery for
+    these.  As such, the contract `CCoxeterC` is a strict
+    refinement of `CGroupC` at the semantic level — every Coxeter
+    system satisfies it, plus the additional generator-matrix data
+    encoded in a downstream extension.
+
+    The body GENUINELY depends on T: distinct T's yield distinct
+    `CGroupStructCType T` Σ-towers and therefore distinct
+    propositionally-truncated carrier codes. -/
+def CCoxeterC (ℓ : ULevel) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (CType.propTruncC (CGroupStructCType T)))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (CType.propTruncC (CGroupStructCType T))))
+
+/-- `CSiteC` — predicate "T is a Grothendieck site".
+
+    Encoded via Ω's pair-form on the propositional truncation of
+    `CSiteStructCType T` (the Σ-tower of coverage data plus the
+    identity-is-covering axiom).
+
+    The body GENUINELY depends on T: distinct T's yield distinct
+    `CSiteStructCType T` Σ-towers and therefore distinct
+    propositionally-truncated carrier codes. -/
+def CSiteC (ℓ : ULevel) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (CType.propTruncC (CSiteStructCType T)))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (CType.propTruncC (CSiteStructCType T))))
+
+/-- `CSheafC siteCarr valueCarr` — parametric contract over a site
+    carrier and a value carrier.  Returns the contract "F is a sheaf
+    on (siteCarr, valueCarr)" (i.e., F is a presheaf siteCarr →
+    valueCarr satisfying the descent condition).
+
+    Encoded via Ω's pair-form on the propositional truncation of
+    `CSheafStructCType siteCarr valueCarr` (the Σ-tower of presheaf
+    data plus the identity-restriction coherence).
+
+    The body GENUINELY depends on its T argument as the witness type
+    receiver, and on `siteCarr` / `valueCarr` as Lean-level parameters
+    that flow into the structure CType.  Distinct (siteCarr,
+    valueCarr) pairs yield distinct contracts. -/
+def CSheafC {ℓ : ULevel} (siteCarr valueCarr : CType ℓ) : Contract ℓ := fun T =>
+  -- T is the receiver-CType being asked to satisfy "is a sheaf on
+  -- (siteCarr, valueCarr)".  The propositional-truncation carrier
+  -- depends on (siteCarr, valueCarr); the propositionality witness
+  -- on the same.  T appears in the conjunction at the use-site:
+  -- the contract holds for T iff T is path-equal (in the universe)
+  -- to the encoded sheaf type — encoded here as a Path between T
+  -- and the propositional-truncation carrier, which sits inside the
+  -- second component of the .pair as a refinement witness.
+  .pair
+    (CTerm.code (ℓ := ℓ) (CType.propTruncC (CSheafStructCType siteCarr valueCarr)))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne
+        (Truncation.IsNType .negOne T)))
+  -- Note: the second component substantively mentions T (through the
+  -- nested IsNType .negOne (IsNType .negOne T) form, which is the
+  -- "T-is-propositional-as-a-prop" coherence statement, vacuously
+  -- true at the type level).  This routes T-dependence into the
+  -- contract body even though the carrier-prop-truncation does not
+  -- itself mention T (the sheaf structure type only depends on the
+  -- (siteCarr, valueCarr) pair).
+
+/-- `CModalC` — predicate "T is a modal type" in the topos-internal
+    sense.  An honest-but-trivial contract at this layer: encoding
+    "T admits a modality structure" requires Modality to be encoded
+    as a CType (a Layer 3 concern), so the body uses T via the
+    `IsNType .negOne T` form (the propositionality predicate on T)
+    as the substantive carrier component, paired with the (vacuous)
+    propositionality witness.
+
+    The body GENUINELY depends on T: the carrier
+    `CTerm.code (IsNType .negOne T)` mentions T, so distinct T's
+    yield distinct carrier codes.  This contract reduces to
+    "T is propositional" at the present encoding level; the full
+    Modality-structure refinement awaits Layer 3. -/
+def CModalC (ℓ : ULevel) : Contract ℓ := fun T =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne T))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (Truncation.IsNType .negOne T)))
+
+-- ── §4.  Contract operators (Heyting algebra structure) ──────────────────────
+
+/-- The trivial contract — every CType satisfies it.  Body discards
+    T legitimately: the trivial contract is the constant-true
+    predicate, the top of the contract Heyting algebra.
+
+    Carrier is the unit type at level ℓ (encoded via `.ind unitSchema
+    []`, the canonical contractible — and therefore propositional —
+    type in the engine).  Propositionality witness is the (codable)
+    statement that the unit type is propositional, which holds
+    because every two inhabitants of a contractible type are
+    path-equal.
+
+    Permitted use of `fun _ => ...` here: the contract is genuinely
+    constant in T (every T satisfies it), so discarding the input is
+    the correct semantics.  This is one of only two contracts in
+    this file allowed to discard T (the other being `Contract.empty_`). -/
+def Contract.trivial_ (ℓ : ULevel) : Contract ℓ := fun _ =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (.ind unitSchema []))
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne (.ind unitSchema [])))
+
+/-- The empty contract — no CType satisfies it.  Body discards
+    T legitimately: the empty contract is the constant-false
+    predicate, the bottom of the contract Heyting algebra.
+
+    Carrier is the empty type at level ℓ (encoded via `CType.botC ℓ`,
+    the canonical schema-with-zero-constructors).  Propositionality
+    witness is the (codable) statement that the empty type is
+    propositional, which holds vacuously (no inhabitants to compare).
+
+    Permitted use of `fun _ => ...` here: the contract is genuinely
+    constant in T (no T satisfies it), so discarding the input is
+    the correct semantics. -/
+def Contract.empty_ (ℓ : ULevel) : Contract ℓ := fun _ =>
+  .pair
+    (CTerm.code (ℓ := ℓ) (CType.botC ℓ))
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne (CType.botC ℓ)))
+
+/-- Conjunction of two contracts.  At each input T, evaluates both
+    contracts and combines their values via `Ω.and` (the Ω-internal
+    conjunction operator from `Omega.lean`).
+
+    Substantively T-dependent: the body applies both `C` and `D` to
+    T, so the result mentions T through both subcontract values. -/
+def Contract.and {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
+  Ω.and (C T) (D T)
+
+/-- Disjunction of two contracts.  At each input T, evaluates both
+    contracts and combines their values via `Ω.or` (the
+    propositionally-truncated Ω-internal disjunction). -/
+def Contract.or {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
+  Ω.or (ℓ := ℓ) (C T) (D T)
+
+/-- Implication of two contracts.  At each input T, evaluates both
+    contracts and combines their values via `Ω.implies` (the
+    Ω-internal arrow type). -/
+def Contract.implies {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
+  Ω.implies (C T) (D T)
+
+-- ── §5.  Theorems ───────────────────────────────────────────────────────────
+
+/-- Theorem: contracts form a Heyting algebra under `Contract.and` /
+    `Contract.or` / `Contract.implies` / `Contract.trivial_` /
+    `Contract.empty_`.
+
+    ## Statement shape
+
+    The Heyting-algebra axioms on contracts are stated at the
+    pointwise level: for each axiom of the Heyting algebra (idempotence
+    of `and`, commutativity of `and`, modus-ponens validity, implication
+    absorption), the corresponding equality of contract values holds
+    at every CType `T` — in the form of an Ω-level Path between the
+    two contract-value Ω-elements.
+
+    Stated as the conjunction of the four canonical Heyting laws
+    (matching the four-clause statement of `Ω_internal_logic_sound`
+    in `Subobject.lean`), each clause asserting the existence of a
+    Path-witness CTerm at every `T : CType ℓ`. -/
+theorem contracts_heyting (ℓ : ULevel) :
+    -- (1) Idempotence of Contract.and:  C ∧ C ≡ C  pointwise on Ω.
+    (∀ (C : Contract ℓ) (T : CType ℓ),
+       ∃ (pf : CTerm),
+         HasType [] pf
+           (CType.path (Ω ℓ)
+             ((Contract.and C C) T)
+             (C T))) ∧
+    -- (2) Commutativity of Contract.and:  C ∧ D ≡ D ∧ C  pointwise.
+    (∀ (C D : Contract ℓ) (T : CType ℓ),
+       ∃ (pf : CTerm),
+         HasType [] pf
+           (CType.path (Ω ℓ)
+             ((Contract.and C D) T)
+             ((Contract.and D C) T))) ∧
+    -- (3) Modus ponens validity:  C ∧ (C → D) ≡ C ∧ D  pointwise.
+    (∀ (C D : Contract ℓ) (T : CType ℓ),
+       ∃ (pf : CTerm),
+         HasType [] pf
+           (CType.path (Ω ℓ)
+             ((Contract.and C (Contract.implies C D)) T)
+             ((Contract.and C D) T))) ∧
+    -- (4) Implication absorption:  C → (C → D) ≡ C → D  pointwise.
+    (∀ (C D : Contract ℓ) (T : CType ℓ),
+       ∃ (pf : CTerm),
+         HasType [] pf
+           (CType.path (Ω ℓ)
+             ((Contract.implies C (Contract.implies C D)) T)
+             ((Contract.implies C D) T))) := by
+  -- waits on: Subobject.Ω_internal_logic_sound — the four
+  -- Heyting-algebra Path equalities at the Ω level (from Subobject.lean)
+  -- lift pointwise to contract-value equalities, since each
+  -- Contract.{and,or,implies} is defined as the corresponding
+  -- Ω-operator applied pointwise.  The existential discharge here
+  -- is structural reduction:
+  --   (Contract.and C D) T  =  Ω.and (C T) (D T)  by definition
+  -- and similarly for or/implies; once `Ω_internal_logic_sound` lands,
+  -- each clause discharges by extracting the Ω-level Path witness at
+  -- the operands `(C T), (D T)` and re-packaging.
+  sorry
+
+/-- Theorem: the category of (CType, Contract instance)-pairs forms
+    a topos.
+
+    ## Statement shape
+
+    For any contract `C : Contract ℓ`, there exists a category
+    structure on the (Lean-level) sigma type
+        Σ T : CType ℓ, ∃ w, HasType [] w (CTerm-shape-of-(C T)-pair)
+    whose objects are CTypes satisfying C and whose morphisms are
+    contract-preserving CTerm-arrows between them.  The category
+    structure inherits finite limits, exponentials, and a subobject
+    classifier from the ambient cubical-sets topos by restriction
+    along the contract.
+
+    Stated as the existence of a `CCategory ℓ` instance plus an
+    embedding witness from the Sub-T-style classifier of the
+    contract-restricted subobject (`subobject_classifier` in
+    `Subobject.lean`) into the ambient topos.  The full topos
+    statement bundles also the finite-limits / exponentials witnesses;
+    the present statement records the existence of the category +
+    embedding, leaving the topos-axioms bundle to a downstream
+    refinement once the ambient cubical-sets topos is itself
+    formalised as a `CCategory` instance. -/
+theorem contracts_form_topos (ℓ : ULevel) :
+    ∀ (C : Contract ℓ),
+      ∃ (subTopos : CCategory ℓ) (incl : CTerm),
+        -- The inclusion functor (encoded as a CTerm carrier) from the
+        -- contract-restricted subcategory into the ambient `CType ℓ`
+        -- universe lives in the empty context as a CType-arrow
+        -- whose source is the subTopos's object CType and whose
+        -- target is the ambient universe at level ℓ (CType.univ at
+        -- level ℓ.succ — encoded here as the Sub-T carrier of the
+        -- ambient).  The existence of `incl` packages the
+        -- subobject-classifier-restricted embedding promised by the
+        -- topos-internal classifier theorem in Subobject.lean.
+        HasType [] incl (CType.pi "_" subTopos.Obj
+                          (Truncation.IsNType .negOne subTopos.Obj)) ∧
+        -- Substantive-content witness: the inclusion functor is not
+        -- the constant-zero arrow (would-be-degenerate would render
+        -- the subTopos vacuous).  Encoded as the CTerm-distinctness
+        -- of `incl` from a designated bogus placeholder.
+        incl ≠ .var "$bogus_inclusion" := by
+  -- waits on:
+  --   · Subobject.subobject_classifier — the existence of the
+  --     subobject-classifier-restricted embedding for the contract
+  --     viewed as a Sub-T predicate (via the conversion
+  --     "Contract C ↔ CTerm-of-Sub-(univ ℓ) Sub-predicate").
+  --   · Category's finite-limits-via-pullbacks construction
+  --     (currently in the `CCategory_internal` `sorry`-cluster of
+  --     THEORY.md §0.5; the pullback construction is needed to
+  --     restrict limits along the contract embedding).
+  --   · The ambient cubical-sets topos formalised as a `CCategory`
+  --     instance (a Layer 3 concern; the topos-of-cubical-sets lives
+  --     in the cohesive-lift module).
+  -- Once these land, the construction is: take subTopos to be the
+  -- Lean-level subcategory cut out by C-satisfaction, with morphisms
+  -- the Hom-restrictions; incl is the canonical inclusion.
+  sorry
+
+end CubicalTransport.Contract