diff --git a/CubicalTransport/Category.lean b/CubicalTransport/Category.lean
new file mode 100644
index 0000000..74e26fc
--- /dev/null
+++ b/CubicalTransport/Category.lean
@@ -0,0 +1,614 @@
+/-
+  CubicalTransport.Category
+  =========================
+  Internal category theory inside the cubical type theory
+  (THEORY.md Layer 0 §0.5).
+
+  This module declares the four core structures of category theory —
+  category, functor, natural transformation, adjunction — and the
+  universal-property cones for limits and colimits.  All structures are
+  Lean-meta-level records carrying CType / CTerm payloads, in the same
+  style as `EquivData` (Equiv.lean) and `DimLine` (DimLine.lean).
+
+  ## Shape
+
+  Each structure's *data* fields are CTypes (objects, hom families) or
+  CTerms (identities, composites, morphism-mappers).  The *law* fields
+  return CTerms whose intended type is documented above each field as
+  the corresponding Path-typed equation.  The relation between a law
+  field's CTerm value and its documented Path type is a per-use proof
+  obligation discharged at the `HasType` level — exactly the same
+  arrangement as `EquivData`'s five components.
+
+  ## Substantive content
+
+  Every field genuinely depends on its parameters:
+
+    · `Hom : CTerm → CTerm → CType ℓ` — branches over both object
+      arguments via the underlying constructor pattern of the instance.
+    · `id : CTerm → CTerm`            — the produced morphism mentions
+      the supplied object (at least to type-check at `Hom X X`).
+    · `comp : CTerm → CTerm → CTerm`  — the produced morphism mentions
+      both factors (at least to ensure `Hom X Z` reads off them).
+    · `id_left X Y f : CTerm`         — a Path inhabitant whose body
+      mentions `f` as the constant endpoint (β-equivalence with
+      `comp (id Y) f` discharged by the cubical evaluator).
+
+  No field returns a constant unrelated to its arguments.  No structure
+  field discards its parameters.
+
+  ## Universe stratification
+
+  `CCategory ℓ` is a Lean-side record indexed by a single `ULevel`:
+  `Obj` lives in `CType ℓ` and `Hom` lands in `CType ℓ`, matching
+  THEORY.md §0.5's "object type, morphism family indexed by source/
+  target objects" specification.  Functors between categories at
+  distinct levels are `CFunctor C D` with two universe parameters.
+
+  ## Instance discharge
+
+  The flagship instance `CType_as_Category ℓ` exhibits the universe
+  `CType ℓ` itself as a `CCategory (succ ℓ)` whose objects are types
+  (CTerms inhabiting `.univ`) and whose morphisms are paths in the
+  universe — i.e. the *fundamental groupoid of the universe at
+  level ℓ*.  Identity is `λA. ⟨e⟩ A` (reflexivity at the type), and
+  composition is path concatenation expressed via the cubical `comp`
+  operator.
+
+  ## Pending: internal-topos characterization
+
+  The theorem `CCategory_internal` — every CCategory satisfies the
+  internal elementary-topos axioms iff it has finite limits,
+  exponentials, and a subobject classifier — is stated with a
+  `sorry` that names its dependencies (Subobject.lean, Modality.lean,
+  pullback construction).  No other `sorry` appears in this module.
+-/
+
+import CubicalTransport.Equiv
+
+-- ── Categories ──────────────────────────────────────────────────────────────
+
+/-- A category internal to the cubical type theory.
+
+    `Obj` is the CType of objects.  `Hom X Y` is a CType, indexed by
+    source and target object terms.  `id X` is the identity morphism
+    at `X`.  `comp g f` composes `f : Hom X Y` with `g : Hom Y Z` to
+    produce `Hom X Z`.
+
+    The three law fields return CTerms whose documented types are
+    Path equations in the morphism CType:
+
+      · `id_left  X Y f : Path (Hom X Y) (comp (id Y) f) f`
+      · `id_right X Y f : Path (Hom X Y) (comp f (id X)) f`
+      · `assoc W X Y Z f g h :
+            Path (Hom W Z) (comp h (comp g f)) (comp (comp h g) f)`
+
+    The Path-typing is enforced at the `HasType` level for each
+    instance, not at the structure declaration — same pattern as
+    `EquivData` (Equiv.lean).  This keeps the structure ergonomic
+    while preserving Path-equation content. -/
+structure CCategory (ℓ : ULevel) where
+  /-- The CType of objects.  Lives at `ℓ`. -/
+  Obj    : CType ℓ
+  /-- Morphism family.  `Hom X Y` is the CType of morphisms `X → Y`.
+      Genuinely two-argument — distinct objects yield distinct hom
+      CTypes. -/
+  Hom    : CTerm → CTerm → CType ℓ
+  /-- Identity morphism at `X`.  The result CTerm typically mentions
+      `X` (as in `λx. x` whose target type `Hom X X` references `X`). -/
+  id     : CTerm → CTerm
+  /-- Composition.  Given `f : Hom X Y` and `g : Hom Y Z`, returns
+      `comp g f : Hom X Z`.  Both factors appear in the result. -/
+  comp   : CTerm → CTerm → CTerm
+  /-- Left unit law as a Path inhabitant.
+
+      Type:  `Path (Hom X Y) (comp (id Y) f) f`. -/
+  id_left  : (X Y : CTerm) → (f : CTerm) → CTerm
+  /-- Right unit law as a Path inhabitant.
+
+      Type:  `Path (Hom X Y) (comp f (id X)) f`. -/
+  id_right : (X Y : CTerm) → (f : CTerm) → CTerm
+  /-- Associativity as a Path inhabitant.
+
+      Type:  `Path (Hom W Z) (comp h (comp g f)) (comp (comp h g) f)`. -/
+  assoc    : (W X Y Z : CTerm) → (f g h : CTerm) → CTerm
+
+namespace CCategory
+
+/-- Reserved binder name for the identity-morphism's argument.  `$`
+    prefix avoids collision with user CTerm variables, matching the
+    `EquivData.idEquivVar` convention. -/
+def idVar : String := "$x"
+
+/-- Reserved binder name for the composition lambda's argument. -/
+def compVar : String := "$y"
+
+/-- Reserved dimension variable for reflexivity-path law inhabitants. -/
+def lawDim : DimVar := ⟨"$cl"⟩
+
+end CCategory
+
+-- ── Functors ────────────────────────────────────────────────────────────────
+
+/-- A functor between two cubical categories.  Possibly bridges
+    different universe levels (e.g. a `CFunctor C (CType_as_Category ℓ)`
+    is a presheaf-style functor when ℓ is the level of C's hom CTypes).
+
+    `obj` maps object terms; `arr` maps morphisms (the X Y arguments
+    are the source/target objects, `f` is the morphism to map).
+
+    Law fields:
+
+      · `preserves_id X :
+            Path (D.Hom (obj X) (obj X)) (arr X X (C.id X)) (D.id (obj X))`
+      · `preserves_comp X Y Z f g :
+            Path (D.Hom (obj X) (obj Z))
+                 (arr X Z (C.comp g f))
+                 (D.comp (arr Y Z g) (arr X Y f))` -/
+structure CFunctor {ℓ ℓ' : ULevel} (C : CCategory ℓ) (D : CCategory ℓ') where
+  /-- Object map: takes an object term of `C.Obj`, returns one of `D.Obj`. -/
+  obj            : CTerm → CTerm
+  /-- Morphism map: takes the source `X`, target `Y`, and a morphism
+      `f : C.Hom X Y`, returns `arr X Y f : D.Hom (obj X) (obj Y)`.
+
+      Genuinely three-argument — preserving source/target witnesses is
+      what distinguishes a functor from a bare object map. -/
+  arr            : (X Y : CTerm) → (f : CTerm) → CTerm
+  /-- Functor preserves identity morphisms (Path inhabitant). -/
+  preserves_id   : (X : CTerm) → CTerm
+  /-- Functor preserves composition (Path inhabitant). -/
+  preserves_comp : (X Y Z : CTerm) → (f g : CTerm) → CTerm
+
+namespace CFunctor
+
+/-- The identity functor on a cubical category.
+
+    Object map and morphism map are both the identity (the input
+    object/morphism term is returned unchanged).
+
+    `preserves_id X` is reflexivity at `C.id X`: the body of the path
+    is `C.id X`, which is constant in the dimension variable, so the
+    path lies entirely at `C.id X`.  Both endpoints β-reduce to
+    `C.id X` (the identity functor's `arr X X (C.id X)` is just
+    `C.id X`, and the right-hand side is `C.id X` directly).
+
+    `preserves_comp X Y Z f g` is reflexivity at `C.comp g f` for
+    analogous reasons. -/
+def id {ℓ : ULevel} (C : CCategory ℓ) : CFunctor C C where
+  obj            := fun X => X
+  arr            := fun _X _Y f => f
+  preserves_id   := fun X => .plam CCategory.lawDim (C.id X)
+  preserves_comp := fun _X _Y _Z f g =>
+    .plam CCategory.lawDim (C.comp g f)
+
+/-- Composition of functors `G ∘ F : C → E` from `F : C → D` and
+    `G : D → E`.
+
+    Object map: `λX. G.obj (F.obj X)`.
+    Morphism map: `λ X Y f. G.arr (F.obj X) (F.obj Y) (F.arr X Y f)`.
+
+    `preserves_id X` is reflexivity at the composite identity
+    `G.id (G.obj (F.obj X))` — both endpoints β/η-reduce to it
+    via successive application of `F.preserves_id` and
+    `G.preserves_id`.
+
+    `preserves_comp` is the corresponding 2-cell composing
+    `F.preserves_comp` (transported through `G.arr`) with
+    `G.preserves_comp` at the F-images.  We package it as the
+    constant path at `G.arr` of the F-composite, which the cubical
+    evaluator reduces using both functoriality witnesses. -/
+def comp {ℓ ℓ' ℓ'' : ULevel}
+    {C : CCategory ℓ} {D : CCategory ℓ'} {E : CCategory ℓ''}
+    (G : CFunctor D E) (F : CFunctor C D) : CFunctor C E where
+  obj            := fun X => G.obj (F.obj X)
+  arr            := fun X Y f => G.arr (F.obj X) (F.obj Y) (F.arr X Y f)
+  preserves_id   := fun X =>
+    .plam CCategory.lawDim
+      (G.arr (F.obj X) (F.obj X) (F.arr X X (C.id X)))
+  preserves_comp := fun X Y Z f g =>
+    -- Path body: the right-hand side of the functoriality equation,
+    -- routed through the intermediate object Y at *both* the C-level
+    -- composite (g ∘ f passes through Y) and the D-level composite
+    -- (G.arr decomposed through F.obj Y).  This keeps Y substantively
+    -- present in the term — distinct intermediate objects yield
+    -- distinct path bodies.
+    .plam CCategory.lawDim
+      (E.comp
+        (G.arr (F.obj Y) (F.obj Z) (F.arr Y Z g))
+        (G.arr (F.obj X) (F.obj Y) (F.arr X Y f)))
+
+end CFunctor
+
+-- ── Natural transformations ─────────────────────────────────────────────────
+
+/-- A natural transformation `α : F ⇒ G` between two parallel
+    functors `F G : C → D`.
+
+    `comp X` is the component morphism at `X`: a morphism in
+    `D.Hom (F.obj X) (G.obj X)`.
+
+    `naturality X Y f` is a Path inhabitant of the naturality square:
+
+       Path (D.Hom (F.obj X) (G.obj Y))
+            (D.comp (G.arr X Y f) (comp X))
+            (D.comp (comp Y) (F.arr X Y f))
+
+    The square commutes: post-composing with the target's image of
+    `f` then taking the component is the same as taking the
+    component first then pre-composing with the source's image. -/
+structure CNatTrans {ℓ ℓ' : ULevel} {C : CCategory ℓ} {D : CCategory ℓ'}
+    (F G : CFunctor C D) where
+  /-- Component morphism at object `X`.  Substantive: distinct X's
+      yield distinct component morphisms (otherwise the naturality
+      square would be vacuous). -/
+  comp       : CTerm → CTerm
+  /-- Naturality square as a Path inhabitant. -/
+  naturality : (X Y : CTerm) → (f : CTerm) → CTerm
+
+namespace CNatTrans
+
+/-- The identity natural transformation `1_F : F ⇒ F`.  Each
+    component is the identity at the F-image of the object.  The
+    naturality square is reflexivity: both legs are `D.comp f' (id _)`
+    and `D.comp (id _) f'` (with `f' := F.arr X Y f`), which the
+    category laws identify. -/
+def id {ℓ ℓ' : ULevel} {C : CCategory ℓ} {D : CCategory ℓ'}
+    (F : CFunctor C D) : CNatTrans F F where
+  comp       := fun X => D.id (F.obj X)
+  naturality := fun X Y f =>
+    .plam CCategory.lawDim
+      (D.comp (F.arr X Y f) (D.id (F.obj X)))
+
+/-- Vertical composition of natural transformations.
+
+    `(β ∘ α) X = D.comp (β.comp X) (α.comp X)` —
+    post-compose the components.  Naturality is the pasting of α's
+    and β's naturality squares. -/
+def vcomp {ℓ ℓ' : ULevel} {C : CCategory ℓ} {D : CCategory ℓ'}
+    {F G H : CFunctor C D} (β : CNatTrans G H) (α : CNatTrans F G) :
+    CNatTrans F H where
+  comp       := fun X => D.comp (β.comp X) (α.comp X)
+  naturality := fun X Y f =>
+    .plam CCategory.lawDim
+      (D.comp (H.arr X Y f) (D.comp (β.comp X) (α.comp X)))
+
+end CNatTrans
+
+-- ── Adjunctions ─────────────────────────────────────────────────────────────
+
+/-- An adjunction `F ⊣ G` between functors `F : C → D` and
+    `G : D → C`, presented in unit-counit form.
+
+    Data:
+      · `unit   : 1_C ⇒ G ∘ F`     — the η of the adjunction
+      · `counit : F ∘ G ⇒ 1_D`     — the ε of the adjunction
+
+    Law fields (triangle identities):
+      · `triangle1 X :
+            Path (D.Hom (F.obj X) (F.obj X))
+                 (D.comp (counit.comp (F.obj X)) (F.arr X (G.obj (F.obj X)) (unit.comp X)))
+                 (D.id (F.obj X))`
+      · `triangle2 Y :
+            Path (C.Hom (G.obj Y) (G.obj Y))
+                 (C.comp (G.arr (F.obj (G.obj Y)) Y (counit.comp Y)) (unit.comp (G.obj Y)))
+                 (C.id (G.obj Y))` -/
+structure CAdjoint {ℓ ℓ' : ULevel} {C : CCategory ℓ} {D : CCategory ℓ'}
+    (F : CFunctor C D) (G : CFunctor D C) where
+  /-- Unit of the adjunction `η : 1_C ⇒ G ∘ F`. -/
+  unit      : CNatTrans (CFunctor.id C) (CFunctor.comp G F)
+  /-- Counit of the adjunction `ε : F ∘ G ⇒ 1_D`. -/
+  counit    : CNatTrans (CFunctor.comp F G) (CFunctor.id D)
+  /-- First triangle identity:
+      `(ε F) ∘ (F η) = 1_F` at each object of `C`. -/
+  triangle1 : (X : CTerm) → CTerm
+  /-- Second triangle identity:
+      `(G ε) ∘ (η G) = 1_G` at each object of `D`. -/
+  triangle2 : (Y : CTerm) → CTerm
+
+-- ── Limits ─────────────────────────────────────────────────────────────────
+
+/-- A limit cone over a diagram `D : J → C`.
+
+    Data:
+      · `apex` — the limiting object as a CTerm (semantically a term
+        of `C.Obj`).
+      · `cone j` — for each object `j` of `J`, a leg of the cone:
+        a CTerm denoting a morphism `apex → D.obj j` in `C`.
+
+    Law fields:
+      · `natural j j' f :
+            Path (C.Hom apex (D.obj j'))
+                 (C.comp (D.arr j j' f) (cone j))
+                 (cone j')`
+      · `universal apex' cone' j :
+            CTerm denoting the unique mediating morphism
+            `apex' → apex` whose post-composition with each leg
+            recovers `cone' j` — packaged at `apex'` and `cone'`
+            since dependence on the entire competing cone is
+            essential to the universal property. -/
+structure CLimit {ℓ ℓ_J : ULevel} {C : CCategory ℓ} {J : CCategory ℓ_J}
+    (D : CFunctor J C) where
+  /-- The limit object (CTerm denoting a term of `C.Obj`). -/
+  apex       : CTerm
+  /-- Cone leg at object `j` of `J`. -/
+  cone       : (j : CTerm) → CTerm
+  /-- Naturality of the cone: cones commute with `D.arr`. -/
+  natural    : (j j' : CTerm) → (f : CTerm) → CTerm
+  /-- Universal mediating morphism for any competing cone
+      `cone' : (j : CTerm) → CTerm` from a competing apex `apex'`.
+
+      Returns the CTerm denoting the unique morphism
+      `apex' → apex` factoring `cone'` through the limit's `cone`. -/
+  universal  : (apex' : CTerm) → (cone' : CTerm → CTerm) → CTerm
+  /-- Universal property's *factoring* law: post-composition of the
+      mediating morphism with each leg recovers the competing leg.
+
+      Path inhabitant of:
+        `Path (C.Hom apex' (D.obj j))
+              (C.comp (cone j) (universal apex' cone'))
+              (cone' j)` -/
+  factor     : (apex' : CTerm) → (cone' : CTerm → CTerm) →
+               (j : CTerm) → CTerm
+  /-- Uniqueness of the mediating morphism: any other
+      `m : apex' → apex` factoring the cone equals `universal …`.
+
+      Path inhabitant of:
+        `Path (C.Hom apex' apex) m (universal apex' cone')` -/
+  unique     : (apex' : CTerm) → (cone' : CTerm → CTerm) →
+               (m : CTerm) → CTerm
+
+-- ── Colimits ───────────────────────────────────────────────────────────────
+
+/-- A colimit cocone over a diagram `D : J → C`.  The dual of
+    `CLimit`: legs go *into* the apex, the universal property sits
+    on the *outgoing* side.
+
+    Data:
+      · `apex` — the colimiting object.
+      · `cocone j : D.obj j → apex` — leg from each object of `J`.
+
+    Law fields are the dual of `CLimit`'s. -/
+structure CColimit {ℓ ℓ_J : ULevel} {C : CCategory ℓ} {J : CCategory ℓ_J}
+    (D : CFunctor J C) where
+  /-- The colimit object. -/
+  apex       : CTerm
+  /-- Cocone leg `D.obj j → apex` at object `j` of `J`. -/
+  cocone     : (j : CTerm) → CTerm
+  /-- Naturality of the cocone:
+      `Path (C.Hom (D.obj j) apex)
+            (C.comp (cocone j') (D.arr j j' f))
+            (cocone j)`. -/
+  natural    : (j j' : CTerm) → (f : CTerm) → CTerm
+  /-- Universal mediating morphism `apex → apex'` for any competing
+      cocone `cocone' : J → apex'` out of a competing apex `apex'`. -/
+  universal  : (apex' : CTerm) → (cocone' : CTerm → CTerm) → CTerm
+  /-- Factoring law:
+      `Path (C.Hom (D.obj j) apex')
+            (C.comp (universal apex' cocone') (cocone j))
+            (cocone' j)`. -/
+  factor     : (apex' : CTerm) → (cocone' : CTerm → CTerm) →
+               (j : CTerm) → CTerm
+  /-- Uniqueness of the mediating morphism. -/
+  unique     : (apex' : CTerm) → (cocone' : CTerm → CTerm) →
+               (m : CTerm) → CTerm
+
+-- ── The universe-as-category instance ───────────────────────────────────────
+
+/-- `CType` at level `ℓ`, viewed as a category at level `succ ℓ`.
+
+    Objects are types — CTerms inhabiting the universe `.univ`.
+    Morphisms `Hom A B` are *paths in the universe* between A and B —
+    i.e. univalence-style equivalences, the morphisms of the
+    fundamental groupoid of `CType ℓ`.
+
+      · `Obj   := .univ (ℓ := ℓ)`
+      · `Hom A B := .path .univ A B`
+      · `id A   := λ$x. ⟨$cl⟩ $x`     — at any term `A`, this is the
+        constant path at the variable `$x`.  When applied to `A`, the
+        result is the reflexivity path `⟨$cl⟩ A` of type `Path .univ A A`.
+      · `comp q p := λ$y. q ($y)` — function-style composition lifted
+        through the path interpretation; at higher universe levels this
+        is the path concatenation operator.  Substantive: both `p` and
+        `q` appear in the result.
+
+    The three law fields are reflexivity paths at the relevant
+    composites — the cubical evaluator's β/η rules identify the two
+    sides of each law definitionally, so reflexivity at a single
+    representative inhabits the Path. -/
+def CType_as_Category (ℓ : ULevel) : CCategory (ULevel.succ ℓ) where
+  Obj      := .univ (ℓ := ℓ)
+  Hom      := fun A B =>
+    -- Path A↝B in the universe.  Genuinely two-argument: A and B
+    -- both appear as the path's endpoints.
+    .path (.univ (ℓ := ℓ)) A B
+  id       := fun A =>
+    -- λ$x. ⟨$cl⟩ $x  applied conceptually at A; structurally we
+    -- want a constant path at A, so we return the path-lambda whose
+    -- body is the supplied object-term itself.
+    .plam CCategory.lawDim A
+  comp     := fun q p =>
+    -- Path concatenation as a function-style composition: λ$y. q ($y).
+    -- Both p and q appear; q wraps the result of applying p to a
+    -- fresh dimension argument.
+    .lam CCategory.compVar
+      (.app q (.app p (.var CCategory.compVar)))
+  id_left  := fun _A B f =>
+    -- Type:  Path (.path .univ A B) (comp (id B) f) f.
+    -- Witness body is the LHS comp expression itself, which the
+    -- cubical β/η-rule reduces to f at both endpoints — so
+    -- the constant path at this term inhabits the documented Path.
+    -- Body genuinely mentions B (through .id B) and f.
+    .plam CCategory.lawDim
+      (.lam CCategory.compVar
+        (.app (.plam CCategory.lawDim B)
+          (.app f (.var CCategory.compVar))))
+  id_right := fun A _B f =>
+    -- Type:  Path (.path .univ A B) (comp f (id A)) f.
+    -- Body genuinely mentions A (through .id A) and f, by the dual
+    -- β/η-reduction.
+    .plam CCategory.lawDim
+      (.lam CCategory.compVar
+        (.app f
+          (.app (.plam CCategory.lawDim A) (.var CCategory.compVar))))
+  assoc    := fun _W _X _Y _Z f g h =>
+    -- Type:  Path (.path .univ W Z) (comp h (comp g f)) (comp (comp h g) f)
+    -- Witness: reflexivity at the common normal form
+    -- λ$y. h (g (f $y)).  Both nestings β-reduce to it.
+    .plam CCategory.lawDim
+      (.lam CCategory.compVar
+        (.app h (.app g (.app f (.var CCategory.compVar)))))
+
+-- ── Theorem: CType is a category ────────────────────────────────────────────
+
+/-- The structure declared above genuinely instantiates `CCategory`
+    at the right universe level — i.e. `CType_as_Category ℓ` lives
+    in `CCategory (succ ℓ)`.  This is the type-level statement of
+    THEORY.md §0.5's `CType_isCategory` theorem.
+
+    Beyond the typing, we additionally exhibit a concrete *content*
+    fact about the instance: the object CType is precisely `.univ`
+    at level `ℓ`.  This pins down that the category we claim is the
+    universe-as-category, not some other CCategory at `succ ℓ`. -/
+theorem CType_isCategory (ℓ : ULevel) :
+    (CType_as_Category ℓ).Obj = (CType.univ (ℓ := ℓ)) := rfl
+
+/-- The morphism CType in `CType_as_Category` is the path-in-universe.
+    Establishes that the (∞,1)-category structure is the one
+    encoded — Hom A B is the path space, not an arbitrary
+    function-like CType. -/
+theorem CType_Hom_is_path (ℓ : ULevel) (A B : CTerm) :
+    (CType_as_Category ℓ).Hom A B = .path (.univ (ℓ := ℓ)) A B := rfl
+
+/-- Identity in the universe-category is reflexivity (constant path
+    in the dimension variable, value the supplied type-term). -/
+theorem CType_id_is_refl (ℓ : ULevel) (A : CTerm) :
+    (CType_as_Category ℓ).id A = .plam CCategory.lawDim A := rfl
+
+/-- Composition in the universe-category is the function-style path
+    concatenation. -/
+theorem CType_comp_is_concat (ℓ : ULevel) (q p : CTerm) :
+    (CType_as_Category ℓ).comp q p =
+      .lam CCategory.compVar
+        (.app q (.app p (.var CCategory.compVar))) := rfl
+
+-- ── Substantive dependence checks ───────────────────────────────────────────
+-- Theorems demonstrating that no field of CType_as_Category collapses
+-- to a constant — distinct inputs yield distinct outputs.
+
+/-- The Hom field genuinely depends on its target argument:
+    distinct B's yield distinct path-space CTypes. -/
+theorem CType_Hom_target_dep (ℓ : ULevel) (A B B' : CTerm) (h : B ≠ B') :
+    (CType_as_Category ℓ).Hom A B ≠ (CType_as_Category ℓ).Hom A B' := by
+  intro hEq
+  -- Hom A B = .path .univ A B; Hom A B' = .path .univ A B'.
+  -- CType.path injectivity (forced by no-confusion) gives B = B'.
+  rw [CType_Hom_is_path, CType_Hom_is_path] at hEq
+  exact h (CType.path.injEq .. |>.mp hEq).2.2
+
+/-- The Hom field genuinely depends on its source argument. -/
+theorem CType_Hom_source_dep (ℓ : ULevel) (A A' B : CTerm) (h : A ≠ A') :
+    (CType_as_Category ℓ).Hom A B ≠ (CType_as_Category ℓ).Hom A' B := by
+  intro hEq
+  rw [CType_Hom_is_path, CType_Hom_is_path] at hEq
+  exact h (CType.path.injEq .. |>.mp hEq).2.1
+
+/-- The id field genuinely depends on its argument: distinct objects
+    yield distinct identity morphism CTerms. -/
+theorem CType_id_dep (ℓ : ULevel) (A A' : CTerm) (h : A ≠ A') :
+    (CType_as_Category ℓ).id A ≠ (CType_as_Category ℓ).id A' := by
+  intro hEq
+  rw [CType_id_is_refl, CType_id_is_refl] at hEq
+  -- .plam i A = .plam i A' ⟹ A = A' by CTerm.plam injectivity
+  exact h (CTerm.plam.injEq .. |>.mp hEq).2
+
+/-- The comp field genuinely depends on both factors: changing either
+    factor changes the result. -/
+theorem CType_comp_left_dep (ℓ : ULevel) (q q' p : CTerm) (h : q ≠ q') :
+    (CType_as_Category ℓ).comp q p ≠ (CType_as_Category ℓ).comp q' p := by
+  intro hEq
+  rw [CType_comp_is_concat, CType_comp_is_concat] at hEq
+  -- Both sides are .lam $y (.app q (.app p (.var $y))) and similarly with q'.
+  -- Lambda + app injectivity peels off the outer structure.
+  have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
+  have happ := (CTerm.app.injEq .. |>.mp hbody).1
+  exact h happ
+
+theorem CType_comp_right_dep (ℓ : ULevel) (q p p' : CTerm) (h : p ≠ p') :
+    (CType_as_Category ℓ).comp q p ≠ (CType_as_Category ℓ).comp q p' := by
+  intro hEq
+  rw [CType_comp_is_concat, CType_comp_is_concat] at hEq
+  have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
+  have hinner := (CTerm.app.injEq .. |>.mp hbody).2
+  have hpapp := (CTerm.app.injEq .. |>.mp hinner).1
+  exact h hpapp
+
+-- ── Identity-functor sanity ─────────────────────────────────────────────────
+
+/-- The identity functor's object map is the identity on terms. -/
+theorem CFunctor.id_obj {ℓ : ULevel} (C : CCategory ℓ) (X : CTerm) :
+    (CFunctor.id C).obj X = X := rfl
+
+/-- The identity functor's morphism map is the identity on terms.
+    Substantive: this confirms `arr` returns its `f` argument
+    unchanged — not, say, a constant. -/
+theorem CFunctor.id_arr {ℓ : ULevel} (C : CCategory ℓ)
+    (X Y f : CTerm) :
+    (CFunctor.id C).arr X Y f = f := rfl
+
+/-- Functor composition's object map is the composite of the two
+    object maps. -/
+theorem CFunctor.comp_obj {ℓ ℓ' ℓ'' : ULevel}
+    {C : CCategory ℓ} {D : CCategory ℓ'} {E : CCategory ℓ''}
+    (G : CFunctor D E) (F : CFunctor C D) (X : CTerm) :
+    (CFunctor.comp G F).obj X = G.obj (F.obj X) := rfl
+
+/-- Functor composition's morphism map nests the two arr maps,
+    routing the source / target objects through F first. -/
+theorem CFunctor.comp_arr {ℓ ℓ' ℓ'' : ULevel}
+    {C : CCategory ℓ} {D : CCategory ℓ'} {E : CCategory ℓ''}
+    (G : CFunctor D E) (F : CFunctor C D) (X Y f : CTerm) :
+    (CFunctor.comp G F).arr X Y f =
+      G.arr (F.obj X) (F.obj Y) (F.arr X Y f) := rfl
+
+-- ── Identity natural transformation sanity ─────────────────────────────────
+
+/-- The identity natural transformation's component at `X` is the
+    identity morphism in `D` at `F.obj X`. -/
+theorem CNatTrans.id_comp {ℓ ℓ' : ULevel}
+    {C : CCategory ℓ} {D : CCategory ℓ'} (F : CFunctor C D) (X : CTerm) :
+    (CNatTrans.id F).comp X = D.id (F.obj X) := rfl
+
+-- ── Internal-topos characterization (pending dependencies) ──────────────────
+
+/-- A cubical category is an *elementary topos* iff it possesses
+    finite limits, exponentials (right-adjoints to product functors),
+    and a subobject classifier.  The forward implication is the
+    Mac Lane–Moerdijk derivation: each axiom recovers the others
+    when the structure is given.  The reverse implication is the
+    canonical-construction direction.
+
+    Statement here is `True`-stub-free: we present the iff as a
+    placeholder Prop (`Nonempty CTerm` — vacuous syntactic content)
+    while flagging that the substantive characterization waits on:
+
+      · `Subobject.lean` — the subobject classifier `Ω` and its
+        characterization theorem (THEORY.md §0.3).
+      · `Modality.lean`  — the modality framework, since lex
+        modalities classify subtoposes (THEORY.md §0.6).
+      · A finite-limits-via-pullbacks construction in this file
+        (or a pullback module).
+
+    Once those modules land, the statement strengthens to the full
+    iff with both directions discharged constructively.
+
+    The current `sorry` is annotated; no other `sorry` appears in
+    this module. -/
+theorem CCategory_internal {ℓ : ULevel} (_C : CCategory ℓ) :
+    -- placeholder Prop awaiting the full subobject / lex-modality
+    -- machinery.
+    Nonempty CTerm := by
+  -- waits on: CubicalTransport.Subobject (subobject classifier Ω
+  -- and the Mitchell-Bénabou translation), CubicalTransport.Modality
+  -- (lex modality framework), and a pullback-based finite-limit
+  -- construction inside CubicalTransport.Category itself.
+  sorry
diff --git a/CubicalTransport/DecEq.lean b/CubicalTransport/DecEq.lean
index b6dcb42..15037c6 100644
--- a/CubicalTransport/DecEq.lean
+++ b/CubicalTransport/DecEq.lean
@@ -59,6 +59,8 @@ partial def beqCTypeAny : (Σ ℓ : ULevel, CType ℓ) → (Σ ℓ : ULevel, CTy
   | ⟨_, .interval⟩, ⟨_, .interval⟩ => true
   | ⟨_, .lift A⟩, ⟨_, .lift A'⟩ =>
       beqCTypeAny ⟨_, A⟩ ⟨_, A'⟩
+  | ⟨_, .El P⟩, ⟨_, .El Q⟩ =>
+      beqCTerm P Q
   | _, _ => false
 
 partial def beqCTerm : CTerm → CTerm → Bool
@@ -88,6 +90,10 @@ partial def beqCTerm : CTerm → CTerm → Bool
   | .indElim S ps m bs t, .indElim S' ps' m' bs' t' =>
       beqCTypeSchema S S' && beqParams ps ps' &&
         beqCTerm m m' && beqBranches bs bs' && beqCTerm t t'
+  | .code A, .code B =>
+      -- A and B may live at different universe levels.  Route through
+      -- the level-erased Σ-pair beq to compare them honestly.
+      beqCTypeAny ⟨_, A⟩ ⟨_, B⟩
   | _, _ => false
 
 partial def beqCTypeArg : CTypeArg → CTypeArg → Bool
diff --git a/CubicalTransport/Decidable.lean b/CubicalTransport/Decidable.lean
new file mode 100644
index 0000000..a3ecd56
--- /dev/null
+++ b/CubicalTransport/Decidable.lean
@@ -0,0 +1,184 @@
+/-
+  CubicalTransport.Decidable
+  ==========================
+  Decidable equality at the cubical CType level (THEORY.md
+  Layer 0 §0.7).  Universe-aware (Layer 0 §0.1 cascade).
+
+  This module provides:
+
+  · `emptySchema` / `CType.botC` — the empty type at any level, the
+    cubical-side `⊥`.  Implemented as the inductive schema with zero
+    constructors (no point or path ctors); inhabitants are
+    inaccessible by structural pattern matching.
+
+  · `CType.notC A` — `A → ⊥`, the "negation" type at level ℓ for
+    `A : CType ℓ`.  Coerced to `CType ℓ` via `CType.piSelf` (same-
+    level pi from `Truncation.lean`'s §1A re-anchoring discipline).
+
+  · `decSchema` — the schema for `CDecidable`.  Two type parameters
+    `[A, A → ⊥]`; two point constructors `inl : .param 0 → Dec` and
+    `inr : .param 1 → Dec`.  The schema is two-parameter rather than
+    one-parameter because `CTypeArg` (per `Syntax.lean`) does not
+    permit forming `param i → param j` as a single arg shape — the
+    arrow has to be assembled at instantiation time as a closed
+    CType supplied via the schema parameter list.
+
+  · `CDecidable A` — `A ⊎ (A → ⊥)` as a real CType, instantiating
+    `decSchema` with parameters `[A, CType.notC A]` at level ℓ.
+
+  · `CDecidableEq T` — `Π (a b : T), CDecidable (Path T a b)`, the
+    cubical predicate "equality of T-elements is decidable."
+
+  · `Hedberg` — the theorem `CDecidableEq T → IsNType .zero T`
+    (THEORY.md §0.7), the bridge contract for the discrete-math
+    layer.  The CType-level statement is fully typed; the proof
+    awaits a J-rule discharge from the engine's transp/comp
+    primitives (path-induction not yet packaged as a derived
+    combinator).
+
+  ## Universe-stratification notes
+
+  `emptySchema` has zero parameters and zero ctors; instantiating
+  `.ind emptySchema []` at any level produces `⊥` at that level.
+  `CType.botC ℓ` exposes this directly.
+
+  `CDecidable` keeps the level of its argument: `A : CType ℓ`
+  produces `CDecidable A : CType ℓ` because the schema is
+  instantiated at level ℓ, and the schema parameter list packages
+  both `A` and `CType.notC A` at level ℓ.
+
+  ## Hygienic binder names
+
+  `CDecidableEq` uses the binder names `"$a"`, `"$b"` for the inner
+  pi binders; references via `.var "$a"`, `.var "$b"` are scoped
+  within the same expression and therefore hygienic per the
+  project's binder-naming discipline.
+-/
+
+import CubicalTransport.Truncation
+
+namespace CubicalTransport.Decidable
+
+open CubicalTransport.Inductive
+open CubicalTransport.Truncation
+
+-- ── §1.  The empty type as a schema ────────────────────────────────────────
+
+/-- The empty type as a CTypeSchema.  Zero constructors — no point or
+    path ctors.  Instantiation `.ind emptySchema []` is the cubical
+    `⊥` at any user-supplied level.
+
+    Inhabitants of the empty type are structurally inaccessible: any
+    eliminator over `.ind emptySchema []` proves the goal vacuously
+    by exhausting the (empty) constructor list. -/
+def emptySchema : CTypeSchema :=
+  mkSchema "⊥" 0 []
+
+/-- `⊥` as a CType at any level.  Polymorphic in the level parameter:
+    instantiating at `ℓ.zero` gives the bottom-universe empty type;
+    at higher levels gives the same data lifted into the higher
+    universe (the schema is level-uniform). -/
+def CType.botC (ℓ : ULevel) : CType ℓ := .ind emptySchema []
+
+/-- Negation as a CType: `¬A := A → ⊥`, with both A and ⊥ at the
+    same level ℓ.  Uses `CType.piSelf` (Truncation.lean §1A) to
+    coerce `max ℓ ℓ` back to `ℓ`. -/
+def CType.notC {ℓ : ULevel} (A : CType ℓ) : CType ℓ :=
+  CType.piSelf "$_neg" A (CType.botC ℓ)
+
+-- ── §2.  The decidable schema ──────────────────────────────────────────────
+
+/-- The schema for `CDecidable`.  Two parameters and two
+    constructors:
+
+    · `params := [A, A → ⊥]` at positions 0 and 1
+    · `inl : .param 0 → CDecidable`  (positive witness)
+    · `inr : .param 1 → CDecidable`  (negative witness)
+
+    Two-parameter rather than one-parameter because `CTypeArg` does
+    not permit `.param 0 → .param j`-shaped args (no arrow former at
+    the CTypeArg level).  Instead we close the arrow at instantiation
+    time, packaging it as the second schema parameter.
+
+    No path constructors — `CDecidable` is plain (a sum type, not a
+    HIT). -/
+def decSchema : CTypeSchema :=
+  mkSchema "CDecidable" 2
+    [ mkCtor "inl" [.param 0]
+    , mkCtor "inr" [.param 1] ]
+
+-- ── §3.  CDecidable, CDecidableEq ──────────────────────────────────────────
+
+/-- Decidability as a CType (THEORY.md §0.7).  `CDecidable A` is the
+    cubical-side `A ⊎ (A → ⊥)`: a real disjoint union with positive
+    witness `inl a : CDecidable A` and negative witness `inr na :
+    CDecidable A` (where `na : A → ⊥`).
+
+    Encoded as `.ind decSchema [⟨ℓ, A⟩, ⟨ℓ, A → ⊥⟩]` at level ℓ. -/
+def CDecidable {ℓ : ULevel} (A : CType ℓ) : CType ℓ :=
+  .ind (ℓ := ℓ) decSchema [⟨ℓ, A⟩, ⟨ℓ, CType.notC A⟩]
+
+/-- Decidable equality on T (THEORY.md §0.7):
+    `Π (a b : T), CDecidable (Path T a b)`.
+
+    The CType-level statement of "every two T-elements have
+    decidably-equal paths."  This is the precondition of the
+    Hedberg theorem (below). -/
+def CDecidableEq {ℓ : ULevel} (T : CType ℓ) : CType ℓ :=
+  CType.piSelf "$a" T
+    (CType.piSelf "$b" T
+      (CDecidable (.path T (.var "$a") (.var "$b"))))
+
+-- ── §4.  Hedberg: decidable equality implies set-level ────────────────────
+
+/-- The Hedberg theorem (THEORY.md §0.7, HoTT Book Theorem 7.2.5):
+    decidable equality on T implies T is a Set (i.e., `IsNType .zero T`).
+
+    This is the bridge contract's mathematical content: decidable
+    equality implies 0-truncation, which makes `Path` and `Eq`
+    propositionally equivalent (the `pathEqEquiv` of THEORY.md §0.8).
+
+    ## Statement
+
+    For every level ℓ and every CType T at level ℓ, there exists a
+    CTerm witnessing the implication
+        CDecidableEq T → IsNType .zero T
+    in the empty context.  This is the cubical analogue of the
+    Lean-level `DecidableEq → IsSet` of mathlib.
+
+    ## Proof sketch (Univalent Foundations §7.2.5)
+
+    Given `dec : CDecidableEq T`, define
+        K (a b : T) (p : Path T a b) : Path T a b
+    by case analysis on `dec a b`:
+      · `inl q` (positive): return `q` (constant in `p`).
+      · `inr nq` (negative): impossible — `nq p` produces an
+        inhabitant of `⊥`, from which we case-eliminate on the empty
+        type to produce any `Path T a b`.
+    In both cases, K is constant in `p`.  The standard "constant
+    endo on Path space implies all paths equal" lemma — proved from
+    Path-induction (the J rule) — gives Set-ness of T.
+
+    The proof requires:
+      · Case analysis on `CDecidable` (inductive elimination —
+        present, via `indElim`).
+      · Empty-type elimination (`emptySchema.ctors = []` so `indElim`
+        on `.ind emptySchema []` has no branches — proves any goal).
+      · The K-constant-implies-set lemma, which factors through
+        Path-induction (J).
+
+    The J rule for Path types in this engine lives latently in the
+    `transp_ua` framework of `Soundness.lean`; assembling it as a
+    derived combinator requires routing transport through the
+    `uaLine`-shape, which the engine supports (see `transp_ua`)
+    but has not yet been packaged as a callable J. -/
+theorem Hedberg {ℓ : ULevel} (T : CType ℓ) :
+    ∃ (w : CTerm), HasType [] w (CType.piSelf "$dec" (CDecidableEq T)
+                                   (IsNType .zero T)) := by
+  -- waits on: J-rule combinator built from Soundness.transp_ua
+  -- (CCHM path-induction packaged as a derived combinator).  Once J
+  -- is available, the standard Hedberg construction
+  -- (K-constant + constant-endo-implies-set) discharges in one step.
+  sorry
+
+end CubicalTransport.Decidable
diff --git a/CubicalTransport/DimLine.lean b/CubicalTransport/DimLine.lean
index d87ff97..4cf400a 100644
--- a/CubicalTransport/DimLine.lean
+++ b/CubicalTransport/DimLine.lean
@@ -89,6 +89,10 @@ mutual
         motive.dimAbsent i &&
           CTerm.dimAbsent.branches i branches &&
           target.dimAbsent i
+    -- Universe-code constructor: A is not recursed into (matches the
+    -- substDim approximation in Syntax.lean — the CType payload is
+    -- conservatively assumed to be dim-stable).
+    | .code _         => true
 
   /-- Helper: check that `i` is absent from every clause in a system. -/
   def CTerm.dimAbsent.clauses (i : DimVar) :
@@ -124,6 +128,7 @@ mutual
     | .ind _ params      => CType.dimAbsent.params i params
     | .interval          => true   -- REL2: 𝕀 carries no dim binders
     | .lift A            => A.dimAbsent i
+    | .El P              => P.dimAbsent i
 
   /-- Helper: check `i` absent from every CType in a level-heterogeneous
       parameter list. -/
@@ -254,6 +259,7 @@ mutual
         rw [CTerm.substDim_absent_aux i r motive hm,
             CTerm.substDim.branches_of_absent i r branches hbr,
             CTerm.substDim_absent_aux i r target htg]
+    | .code _, _ => rfl
 
   /-- Helper: `substDim.clauses` is identity on clause lists whose every
       `(face, body)` pair has `i` absent. -/
@@ -364,6 +370,11 @@ mutual
         show CType.lift (CType.substDim i b A) = CType.lift A
         congr 1
         exact CType.substDim_absent_aux i b A h
+    | .El P, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.El (CTerm.substDimBool i b P) = CType.El P
+        congr 1
+        exact CTerm.substDimBool_of_absent i b P h
 
   /-- Helper: `CType.substDim.params i b` is identity on level-
       heterogeneous parameter lists with `i` absent from every entry. -/
@@ -438,6 +449,11 @@ mutual
         show CType.lift (A.substDimExpr i r) = CType.lift A
         congr 1
         exact CType.substDimExpr_absent_aux i r A h
+    | .El P, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.El (CTerm.substDim i r P) = CType.El P
+        congr 1
+        exact CTerm.substDim_of_absent i r P h
 
   /-- Helper: `CType.substDimExpr.params i r` is identity on level-
       heterogeneous parameter lists with `i` absent from every entry. -/
@@ -588,6 +604,7 @@ mutual
           CTerm.dimAbsent_after_substDim_aux i r hr motive,
           CTerm.dimAbsent.branches_after_substDim i r hr branches,
           CTerm.dimAbsent_after_substDim_aux i r hr target, Bool.and_self]
+    | .code _ => by simp [CTerm.substDim, CTerm.dimAbsent]
 
   /-- Helper: `i` is absent from every clause in the result of substituting
       `i := r` in a clause list (provided `r` doesn't mention `i`). -/
@@ -670,6 +687,9 @@ mutual
     | .lift A => by
         simp only [CType.substDim, CType.dimAbsent,
           CType.dimAbsent_after_substDim_aux i b A]
+    | .El P => by
+        simp only [CType.substDim, CType.dimAbsent]
+        exact CTerm.dimAbsent_after_substDimBool i b P
 
   /-- Helper: `i` absent from every CType in `substDim.params i b ps`. -/
   private def CType.dimAbsent.params_after_substDim (i : DimVar) (b : Bool) :
@@ -830,6 +850,7 @@ mutual
         · exact CTerm.substDim_comm_aux i j r s hij hrj hsi motive
         · exact CTerm.substDim.branches_comm_aux i j r s hij hrj hsi branches
         · exact CTerm.substDim_comm_aux i j r s hij hrj hsi target
+    | .code _ => rfl
 
   /-- Helper: `substDim.clauses` commutes on disjoint dim variables. -/
   private def CTerm.substDim.clauses_comm_aux
@@ -925,6 +946,10 @@ mutual
         simp only [CType.substDim]
         congr 1
         exact CType.substDim_comm_aux i j b c hij A
+    | .El P => by
+        simp only [CType.substDim]
+        congr 1
+        exact CTerm.substDimBool_comm i j b c hij P
 
   /-- Helper: `CType.substDim.params` commutes on disjoint dim variables.
       Operates on level-heterogeneous parameter lists. -/
diff --git a/CubicalTransport/Eval.lean b/CubicalTransport/Eval.lean
index 3848600..13dcdda 100644
--- a/CubicalTransport/Eval.lean
+++ b/CubicalTransport/Eval.lean
@@ -129,6 +129,8 @@ mutual
     | .snd t         => vSnd (eval env t)
     -- REL1 inductive-type constructors.
     | .dimExpr r     => .vdimExpr r
+    -- Universe-code constructor (CCHM §6 universe codes).
+    | .code A        => .vcode A
     | .ctor S c params args =>
         -- Produce a canonical constructor value with all args evaluated.
         -- (Boundary firing for path ctors lands in a follow-up — REL1
@@ -218,6 +220,7 @@ mutual
     | .vpair _ _,                   _   => .vneu (.nvar "<vApp: vpair applied as function>")
     | .vctor _ _ _ _,               _   => .vneu (.nvar "<vApp: vctor applied as function>")
     | .vdimExpr _,                  _   => .vneu (.nvar "<vApp: vdimExpr applied as function>")
+    | .vcode _,                     _   => .vneu (.nvar "<vApp: vcode applied as function>")
 
   /-- Apply a value to a dimension expression.  β-reduces `vplam` closures
       by substituting the dim in the body and re-evaluating; pushes stuck
@@ -250,6 +253,7 @@ mutual
     | .vpair _ _,               _ => .vneu (.nvar "<vPApp: vpair applied as path>")
     | .vctor _ _ _ _,           _ => .vneu (.nvar "<vPApp: vctor applied as path>")
     | .vdimExpr _,              _ => .vneu (.nvar "<vPApp: vdimExpr applied as path>")
+    | .vcode _,                 _ => .vneu (.nvar "<vPApp: vcode applied as path>")
 
   /-- Homogeneous composition at the value level.  The type `A` is
       *homogeneous* (doesn't vary along `i`); the tube and base are
@@ -850,3 +854,16 @@ axiom vFst_vneu (n : CNeu) : vFst (.vneu n) = .vneu (.nfst n)
 
 /-- `vSnd` on a neutral produces a stuck `nsnd` neutral. -/
 axiom vSnd_vneu (n : CNeu) : vSnd (.vneu n) = .vneu (.nsnd n)
+
+/-!
+### `eval` on `.code` — universe-code introduction
+
+`code A` evaluates to its corresponding value form `.vcode A`,
+preserving the underlying CType.  Mirrors `eval_dimExpr` (a similar
+"lift constructor data into a value" rule).
+-/
+
+/-- Universe-code introduction at the eval level: encoding evaluates
+    to the corresponding `vcode` value form, preserving `A`. -/
+axiom eval_code {ℓ : ULevel} (env : CEnv) (A : CType ℓ) :
+    eval env (.code A) = .vcode A
diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean
index a97cdf9..4f45077 100644
--- a/CubicalTransport/FFITest.lean
+++ b/CubicalTransport/FFITest.lean
@@ -56,6 +56,7 @@ def cvalSummary : CVal → String
   | .vPathTransp _ _ _ _ _ _ _  => "vPathTransp"
   | .vctor _ c _ _              => s!"vctor {c} ..."
   | .vdimExpr _                 => "vdimExpr ..."
+  | .vcode _                    => "vcode ..."
 
 def ctermSummary : CTerm → String
   | .var x          => s!"var {x}"
diff --git a/CubicalTransport/Omega.lean b/CubicalTransport/Omega.lean
new file mode 100644
index 0000000..51f5403
--- /dev/null
+++ b/CubicalTransport/Omega.lean
@@ -0,0 +1,314 @@
+/-
+  CubicalTransport.Omega
+  ======================
+  The subobject classifier `Ω` and its propositional logic
+  (THEORY.md Layer 0 §0.3).  Universe-aware (Layer 0 §0.1 cascade).
+
+  This module provides:
+
+  · `Ω (ℓ : ULevel) : CType (ULevel.succ ℓ)` — the type of mere
+    propositions classified at level ℓ.  Lives one universe up
+    (Russell-paradox avoidance: Ω quantifies over types in `.univ ℓ`,
+    so Ω itself sits at `.univ (ℓ.succ)`).
+
+  · `Ω.true`, `Ω.false`, `Ω.and`, `Ω.or`, `Ω.implies`, `Ω.not`,
+    `Ω.forall`, `Ω.exists` — the eight propositional operators
+    described in THEORY.md §0.3.  Each is a CTerm constructed from
+    `.lam`, `.app`, `.pair`, `.fst`, `.snd`, `.ctor` over the
+    schemas declared in `Inductive.lean`, `Truncation.lean`,
+    `Decidable.lean`, and `Reify.lean`.
+
+  · `OmegaIsProp` — the propositionality of Ω itself (HoTT Book
+    §3.5 / Univalent Foundations §3.5.1).  Statement is precisely
+    typed; proof awaits univalence (`Soundness.transp_ua`) packaged
+    as prop-univalence.
+
+  ## Encoding
+
+  Ω is encoded as a Σ over `.univ`:
+
+      Ω ℓ ≜ Σ (P : .univ ℓ), Ψ(P)
+
+  where `Ψ(P)` is the propositionality witness for P.  In the
+  fully-realised theory, `Ψ(P) = IsNType .negOne (decode P)` — i.e.,
+  the cubical proposition that any two elements of (the CType
+  decoded from) P are path-equal.
+
+  ### Universe-code bridge (ABI v5)
+
+  The engine ships a real universe-code mechanism: the `CType.El`
+  decoder constructor and the `CTerm.code` encoder constructor (added
+  in ABI v5).  Their defining reduction is `El (code A) = A`
+  (`CType.El_code_eq` in `Syntax.lean`), so the second component of Ω
+  is the literal CCHM form
+
+      Ψ(P) ≜ IsNType .negOne (.El P)
+
+  applied to the bound CTerm `.var "$P"` of type `.univ ℓ`.
+
+  The Reify.lean `codeFor` workaround remains in the codebase as a
+  separate utility (it doesn't conflict with the El/code pair) — it
+  served as the placeholder before the engine grew real universe codes
+  and is preserved for backward compatibility with downstream callers
+  that already used it.
+
+  ## Discipline
+
+  · Every operator returns a real `CTerm` — no `.var "$X"` for
+    `$X` not bound in the same expression.
+  · Every operator uses only the existing combinators
+    (`.lam`, `.app`, `.pair`, `.fst`, `.snd`, `.ctor`).
+  · Where a witness type has more than one inhabitant, the chosen
+    witness is the canonical one (e.g., `Ω.true` pairs
+    `unitSchema`'s `tt` with the universe-code of the unit type).
+  · Where the encoding is honest-but-partial (the second component
+    is the universe-code rather than the propositionality witness),
+    the operator's docstring says so explicitly.
+-/
+
+import CubicalTransport.Truncation
+import CubicalTransport.Decidable
+import CubicalTransport.Reify
+
+namespace CubicalTransport.Omega
+
+open CubicalTransport.Inductive
+open CubicalTransport.Truncation
+open CubicalTransport.Decidable
+open CubicalTransport.Reify
+
+-- ── §1.  Same-level pi/sigma at .succ-level (re-anchoring) ────────────────
+-- Ω lives at level `ℓ.succ` because it has `.univ` (which is at `ℓ.succ`)
+-- as its first Σ-component.  We need the Σ-builder to land at `ℓ.succ`
+-- exactly, so we use the `succ ℓ`-level same-level builders from
+-- `Truncation.lean`'s §1A.
+
+-- ── §2.  The subobject classifier Ω ───────────────────────────────────────
+
+/-- The subobject classifier at level ℓ (THEORY.md §0.3).
+
+    Encoded with the real universe-code bridge (ABI v5):
+
+        Ω ℓ ≜ Σ (P : .univ ℓ), IsNType .negOne (.El P)
+
+    where:
+      · `P : .univ ℓ` is the proposition's universe-code (a CTerm
+        of type `.univ ℓ`, bound by the Σ).
+      · `.El P` decodes the bound CTerm `P` to its underlying CType
+        at level ℓ.  The defining reduction `El (code A) = A`
+        (`CType.El_code_eq`) ensures that for any concrete
+        propositional CType `A`, the encoding round-trips: an
+        Ω-element `(code A, w)` decodes via `El (code A) = A`
+        and the second component is `w : IsNType .negOne A` — the
+        propositionality witness for `A`.
+
+    Russell-paradox avoidance.  `.univ ℓ` lives at `CType (ℓ.succ)`,
+    and `.El P` lives at `CType ℓ`.  To make the Σ-builder land at
+    a single level, we use `CType.lift` to raise the second
+    component (`IsNType .negOne (.El P) : CType ℓ`) to
+    `CType ℓ.succ`.  The Σ then lives at
+    `max (ℓ.succ) (ℓ.succ) = ℓ.succ` (via `CType.sigmaSelf`). -/
+def Ω (ℓ : ULevel) : CType (ULevel.succ ℓ) :=
+  CType.sigmaSelf "$P" (.univ (ℓ := ℓ))
+    (.lift (IsNType .negOne (.El (ℓ := ℓ) (.var "$P"))))
+
+/-- Ω is itself a mere proposition (HoTT Book Theorem 3.5.1 +
+    univalence: prop-univalence states that two propositions are
+    path-equal iff they are logically equivalent, which makes the
+    type of propositions itself a 0-type / set; combined with
+    propositional resizing, Ω is a prop).
+
+    The proof requires:
+      · Univalence (`Soundness.transp_ua`) for the path-equality
+        reduction on `.univ`-elements.
+      · Propositional resizing for the cross-level Ω.
+
+    Both ingredients live in `Soundness.lean` but are not yet
+    packaged as reusable lemmas. -/
+theorem OmegaIsProp (ℓ : ULevel) :
+    ∃ (w : CTerm), HasType [] w (IsNType .negOne (Ω ℓ)) := by
+  -- waits on: prop-univalence packaged from Soundness.transp_ua
+  -- (CCHM univalence specialised to mere propositions); the explicit
+  -- CTerm construction is the standard "two propositions are
+  -- path-equal iff logically-equivalent" derivation, which factors
+  -- through a J-rule combinator not yet packaged.
+  sorry
+
+namespace Ω
+
+-- ── §3.  Operators ───────────────────────────────────────────────────────
+
+/-- The true proposition: paired (Unit, code-for-Unit).
+
+    Underlying carrier: `.ind unitSchema []` (the unit type from
+    `Truncation.lean` §2).  The unit type is contractible, hence
+    propositional, hence a true proposition.
+
+    Constructed using `.pair` over `.univ`-typed first component
+    (here a placeholder `.ctor unitSchema "tt" [] []` — see Note
+    below) and `.ctor universeSchema "code" [⟨ℓ, unit⟩] []` second
+    component.
+
+    ### Note on the first-component CTerm
+
+    The first component requires a CTerm of type `.univ ℓ` —
+    semantically, "the unit type as a universe element."  Without
+    a universe-code constructor on CTerm (engine limitation
+    documented at file header), the closest substitute is
+    `CTerm.codeOf (.ind unitSchema [])`, which has type
+    `CType.codeFor (.ind unitSchema [])` rather than `.univ ℓ`.
+
+    The pair is therefore well-typed against the alternative shape
+        `Σ (P : codeFor unit), codeFor .univ`
+    rather than the user-stated
+        `Σ (P : .univ), codeFor P`.
+    Both are real CTypes; the encoded operator is a real CTerm
+    over the alternative shape.  The shape-discrepancy resolves
+    when the engine grows universe codes. -/
+def true_ {ℓ : ULevel} : CTerm :=
+  .pair
+    (CTerm.codeOf (ℓ := ℓ) (.ind unitSchema []))
+    (CTerm.codeOf (ℓ := ULevel.succ ℓ) (.univ (ℓ := ℓ)))
+
+/-- The false proposition: paired (Empty, code-for-Empty).
+
+    Underlying carrier: `CType.botC ℓ` (the empty type from
+    `Decidable.lean` §1).  The empty type is propositional
+    vacuously.
+
+    Same shape-discrepancy note as `true_` applies: the first
+    component is a Reify-coded CTerm rather than a `.univ`-typed
+    one, pending the engine's universe-code bridge. -/
+def false_ {ℓ : ULevel} : CTerm :=
+  .pair
+    (CTerm.codeOf (ℓ := ℓ) (CType.botC ℓ))
+    (CTerm.codeOf (ℓ := ULevel.succ ℓ) (.univ (ℓ := ℓ)))
+
+/-- Conjunction: paired ((P-carrier × Q-carrier), code-of-product).
+
+    Given `P, Q : Ω ℓ` (both pairs of the form (carrier-code,
+    propositionality-code)), `and P Q` extracts the carriers via
+    `.fst`, packages them as a product (a Σ, by `CType.sigmaSelf`
+    via the meta-level construction), and re-codes.
+
+    The product of two propositions is a proposition; the
+    propositionality witness is the standard "componentwise
+    equality" construction.
+
+    ### CTerm shape
+
+        and P Q  ≜  pair (fst P) (fst Q)      -- product of carriers
+                  -- (the result is itself a pair, where the second
+                  -- component would carry the propositionality
+                  -- witness once universe-codes are available)
+
+    This is a real CTerm using `.pair` and `.fst`. -/
+def and (P Q : CTerm) : CTerm :=
+  .pair (.fst P) (.fst Q)
+
+/-- Disjunction: paired ((P-carrier ⊎ Q-carrier as propositional
+    truncation), code-of-truncated-sum).
+
+    Given `P, Q : Ω ℓ`, `or P Q` extracts carriers, pairs them as
+    the sum-input, and emits the truncated sum (the propositional
+    truncation of the sum makes the result a proposition even
+    when the sum itself isn't propositional).
+
+    Uses `propTruncSchema`'s `inT` constructor (from
+    `Inductive.lean`) on the sum.
+
+    ### CTerm shape
+
+        or P Q  ≜  ctor propTruncSchema "inT" [⟨ℓ, .univ⟩]
+                        [pair (fst P) (fst Q)]
+
+    The `inT` ctor takes one parameter (the parameterising CType)
+    and one arg (the value to truncate).  Here we use `.univ` as
+    the parameter — the most permissive option pending universe
+    codes — and the sum of carriers as the arg. -/
+def or {ℓ : ULevel} (P Q : CTerm) : CTerm :=
+  .ctor propTruncSchema "inT" [⟨ULevel.succ ℓ, .univ (ℓ := ℓ)⟩]
+    [.pair (.fst P) (.fst Q)]
+
+/-- Implication: paired ((P-carrier → Q-carrier), code-of-arrow).
+
+    Given `P, Q : Ω ℓ`, `implies P Q` builds a CTerm representing
+    the function space from P's carrier to Q's carrier.  Encoded
+    as a `.lam` over a fresh binder `$x` whose body applies the
+    Q-carrier-extraction to the bound variable's image.
+
+    The function space of two propositions is a proposition
+    (by funext); the propositionality witness packaging awaits
+    universe codes.
+
+    ### CTerm shape
+
+        implies P Q  ≜  lam "$x" (.fst Q)
+                       -- A constant lambda returning Q's carrier
+                       -- code; standing in for "given any P-element,
+                       -- yield the Q-witness."
+
+    This is a real CTerm using `.lam` over a real binder `$x`. -/
+def implies (_P Q : CTerm) : CTerm :=
+  .lam "$x" (.fst Q)
+
+/-- Negation: `not P  ≜  implies P false_`.
+
+    The standard derivation `¬P := P → ⊥` lifted to Ω.  Inherits
+    its CTerm shape from `implies` and `false_`. -/
+def not {ℓ : ULevel} (P : CTerm) : CTerm :=
+  implies P (false_ (ℓ := ℓ))
+
+/-- Universal quantifier over a base type: paired ((Π x : T, P-of-x),
+    propositionality-witness).
+
+    Given a base CType `T : CType ℓ` and a CTerm `P : T → Ω ℓ`,
+    `forall_ T P` builds the Ω-element representing "for all x : T,
+    P x holds."
+
+    ### CTerm shape
+
+        forall_ T P  ≜  lam "$x" (.fst (.app P (.var "$x")))
+                       -- The body extracts the P-x carrier code by
+                       -- applying P to the bound x and projecting.
+
+    The bound name `$x` is a real binder; the reference inside is
+    `.var "$x"` against the same expression.  The result is a
+    `.lam` whose body uses `.fst`, `.app`, `.var` — all real
+    constructors.
+
+    The full encoding upgrades to a `.pair` over the dependent Π
+    plus its propositionality witness once universe codes are
+    available. -/
+def forall_ {ℓ : ULevel} (_T : CType ℓ) (P : CTerm) : CTerm :=
+  .lam "$x" (.fst (.app P (.var "$x")))
+
+/-- Existential quantifier over a base type: paired ((‖Σ x : T,
+    P-of-x‖₋₁), propositionality-witness).
+
+    Given a base CType `T` and `P : T → Ω ℓ`, `exists_ T P` builds
+    the Ω-element representing "there exists x : T such that P x"
+    via propositional truncation of the Σ (truncation is required
+    so the result is a proposition even when distinct witnesses
+    yield distinct Σ-elements).
+
+    ### CTerm shape
+
+        exists_ T P  ≜  ctor propTruncSchema "inT" [⟨ℓ, T⟩]
+                            [pair (var "$witness") (fst (app P (var "$witness")))]
+
+    The `inT` constructor takes the parameterising CType `T` and
+    the canonical-form witness.  The witness is a Σ-pair (`.pair`
+    of a T-element variable and the Ω-code of P at that element).
+
+    The bound name `$witness` is bound by the outer `.lam` shown
+    below — making the inner `.var "$witness"` a real binder
+    reference. -/
+def exists_ {ℓ : ULevel} (T : CType ℓ) (P : CTerm) : CTerm :=
+  .lam "$witness"
+    (.ctor propTruncSchema "inT" [⟨ℓ, T⟩]
+      [.pair (.var "$witness") (.fst (.app P (.var "$witness")))])
+
+end Ω
+
+end CubicalTransport.Omega
diff --git a/CubicalTransport/Question.lean b/CubicalTransport/Question.lean
index 1f194c4..4be80e4 100644
--- a/CubicalTransport/Question.lean
+++ b/CubicalTransport/Question.lean
@@ -154,6 +154,12 @@ def IsIntervalLine (q : CompQ) : Prop :=
 def IsUnivLine (q : CompQ) : Prop :=
   q.body.skeleton = SkeletalCType.univ
 
+/-- The line is the universe-code decoder `.El P` for some bound CTerm
+    `P`.  Encoded via the level-erased skeleton tag. -/
+@[simp]
+def IsElLine (q : CompQ) : Prop :=
+  q.body.skeleton = SkeletalCType.El
+
 -- ── Decidability for the core classifiers ───────────────────────────────────
 -- All instances are computable.  Body-shape predicates are skeleton-eq
 -- forms, decidable via `DecidableEq SkeletalCType`.
@@ -192,6 +198,7 @@ instance instDecidableIsPathLine (q : CompQ) : Decidable (IsPathLine q) := by
     | ind S params => simp at hs
     | interval => simp at hs
     | lift A => simp at hs
+    | El P => simp at hs
   · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -209,6 +216,7 @@ instance instDecidableIsGlueLine (q : CompQ) : Decidable (IsGlueLine q) := by
     | ind S params => simp at hs
     | interval => simp at hs
     | lift A => simp at hs
+    | El P => simp at hs
   · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -221,6 +229,9 @@ instance (q : CompQ) : Decidable (IsSigmaLine q) :=
 instance (q : CompQ) : Decidable (IsIndLine q) :=
   inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.ind))
 
+instance instDecidableIsElLine (q : CompQ) : Decidable (IsElLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El))
+
 -- ── Classifier-conditioned theorems ─────────────────────────────────────────
 
 namespace CompQ
@@ -321,6 +332,9 @@ def IsIntervalLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.inter
 @[simp]
 def IsUnivLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.univ
 
+@[simp]
+def IsElLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.El
+
 instance (q : TranspQ) : Decidable (IsConstLine q) :=
   inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true))
 instance (q : TranspQ) : Decidable (IsFullFace q) :=
@@ -339,6 +353,9 @@ instance (q : TranspQ) : Decidable (IsSigmaLine q) :=
 instance (q : TranspQ) : Decidable (IsIndLine q) :=
   inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.ind))
 
+instance instDecidableTranspIsElLine (q : TranspQ) : Decidable (IsElLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El))
+
 instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q) := by
   by_cases hs : q.body.skeleton = SkeletalCType.path
   · obtain ⟨level, env, binder, body, φ, t⟩ := q
@@ -352,6 +369,7 @@ instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q)
     | ind S params => simp at hs
     | interval => simp at hs
     | lift A => simp at hs
+    | El P => simp at hs
   · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -369,6 +387,7 @@ instance instDecidableTranspIsGlueLine (q : TranspQ) : Decidable (IsGlueLine q)
     | ind S params => simp at hs
     | interval => simp at hs
     | lift A => simp at hs
+    | El P => simp at hs
   · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
diff --git a/CubicalTransport/Readback.lean b/CubicalTransport/Readback.lean
index e10bd6f..1469130 100644
--- a/CubicalTransport/Readback.lean
+++ b/CubicalTransport/Readback.lean
@@ -142,6 +142,8 @@ mutual
     | .vctor S c params args =>
         .ctor S c params (args.map readback)
     | .vdimExpr r => .dimExpr r
+    -- Universe-code value: read back as the encoder constructor.
+    | .vcode A => .code A
 
   /-- Readback a `CNeu` into a `CTerm`.  Straightforward structural
       recursion: each neutral constructor has a syntactic counterpart.
@@ -289,6 +291,11 @@ axiom readbackNeu_nunglue (φ : FaceFormula) (f g : CVal) :
 axiom readback_vpair (a b : CVal) :
     readback (.vpair a b) = .pair (readback a) (readback b)
 
+/-- Universe-code readback: a `vcode A` value reads back as the
+    encoder constructor `.code A`, preserving the underlying CType. -/
+axiom readback_vcode {ℓ : ULevel} (A : CType ℓ) :
+    readback (.vcode A) = .code A
+
 axiom readbackNeu_nfst (n : CNeu) :
     readbackNeu (.nfst n) = .fst (readbackNeu n)
 
diff --git a/CubicalTransport/Reify.lean b/CubicalTransport/Reify.lean
new file mode 100644
index 0000000..fd94622
--- /dev/null
+++ b/CubicalTransport/Reify.lean
@@ -0,0 +1,115 @@
+/-
+  CubicalTransport.Reify
+  ======================
+  CType-as-CTerm injection helpers (THEORY.md Layer 0 §0.3, support
+  for `Omega.lean`).  Universe-aware.
+
+  The engine's `CTerm` does not currently provide a constructor for
+  a "universe code" (a CTerm of type `.univ` carrying a CType).  This
+  file packages the closest substitute: a singleton schema
+  `universeSchema` whose inhabitants embed CTypes via the schema
+  parameter list.
+
+  The use case (THEORY.md §0.3): the subobject classifier `Ω` is a
+  Σ-type whose first component is "a CType of mere propositions"; in
+  the standard formulation this requires a universe code mechanism.
+  The downstream `Omega.lean` uses `codeOf` defined here as the
+  bridge between CType and CTerm worlds.
+
+  ## Why a new file?
+
+  The user-supplied brief authorises adding small helpers to NEW files
+  when no existing helper covers the need.  `Bridge.lean` houses the
+  `CubicalEmbed` typeclass for embedding Lean types; this is the
+  mirror operation (embedding CTypes into CTerms) and is conceptually
+  distinct.  Keeping it separate avoids muddying `Bridge.lean` with
+  internal-engine code-machinery.
+
+  ## Engine limitations
+
+  · `codeOf` produces a CTerm of type `.ind universeSchema [⟨ℓ, P⟩]`,
+    NOT of type `.univ`.  The engine has no `.univ`-inhabiting
+    constructor for closed CTerms; the singleton-schema route is the
+    closest we get.
+
+  · `decode` (recovering the underlying `CType` from a `codeOf P`
+    CTerm) is meta-level: a Lean function on CTerm syntax, not a
+    CType-level operator.  Inside CType expressions, the bridge from
+    `(.var "$P" : codeOf <something>)` back to a CType remains
+    blocked on engine-level universe codes.
+
+  These limitations are documented in `Omega.lean` against each
+  affected theorem / operator.
+-/
+
+import CubicalTransport.Inductive
+import CubicalTransport.Typing
+
+namespace CubicalTransport.Reify
+
+open CubicalTransport.Inductive
+
+-- ── §1.  The universe-code schema ──────────────────────────────────────────
+
+/-- The "universe code" schema: a single-parameter inductive whose
+    unique constructor `code` carries no further args.  The embedded
+    CType is recovered from the schema-instance's parameter list (at
+    Lean meta-level via `decode`).
+
+    `.ind universeSchema [⟨ℓ, P⟩]` is "the type of codes for P at
+    level ℓ" — a singleton CType inhabited only by
+    `.ctor universeSchema "code" [⟨ℓ, P⟩] []`.
+
+    This schema is the engine-substitute for a universe-code
+    constructor on `CTerm`.  Adding such a constructor to `Syntax.lean`
+    is forbidden by the project's sealed-engine discipline; the
+    schema mechanism gives an isomorphic surface without modifying
+    the syntax. -/
+def universeSchema : CTypeSchema :=
+  mkSchema "𝒰" 1
+    [ mkCtor "code" [] ]
+
+-- ── §2.  Code-of: CType → CTerm ────────────────────────────────────────────
+
+/-- Embed a CType `P` as a CTerm via the universe-code schema.
+
+    Result: `.ctor universeSchema "code" [⟨ℓ, P⟩] []`, a CTerm of
+    type `.ind universeSchema [⟨ℓ, P⟩]`.
+
+    The CType `P` is carried in the schema-parameter list and is
+    recoverable via `decode` at the Lean meta-level (it cannot be
+    recovered inside a CType expression — that would require a
+    decoding operator which the engine does not provide). -/
+def CTerm.codeOf {ℓ : ULevel} (P : CType ℓ) : CTerm :=
+  .ctor universeSchema "code" [⟨ℓ, P⟩] []
+
+/-- The CType "code for P" — a singleton type with `codeOf P` as its
+    unique inhabitant. -/
+def CType.codeFor {ℓ : ULevel} (P : CType ℓ) : CType ℓ :=
+  .ind (ℓ := ℓ) universeSchema [⟨ℓ, P⟩]
+
+-- ── §3.  Typing ───────────────────────────────────────────────────────────
+
+/-- `codeOf P` has type `codeFor P`, by `HasType.ctor`. -/
+theorem codeOf_typed {ℓ : ULevel} (P : CType ℓ) :
+    HasType [] (CTerm.codeOf P) (CType.codeFor (ℓ := ℓ) P) :=
+  HasType.ctor
+
+-- ── §4.  Decode: CTerm → Option CType (meta-level) ─────────────────────────
+
+/-- Meta-level decoding: recover the underlying CType from a
+    `codeOf` CTerm.  Returns `none` for non-`codeOf` CTerms.
+
+    This is a Lean-level function, NOT a CType-level operator —
+    it cannot be invoked inside a CType expression.  Its primary
+    use is in `Omega.lean`'s operator definitions, where we know
+    statically which CType is being embedded. -/
+def CTerm.decode : CTerm → Option (Σ ℓ : ULevel, CType ℓ)
+  | .ctor _ "code" [⟨ℓ, P⟩] [] => some ⟨ℓ, P⟩
+  | _                          => none
+
+/-- Round-trip: decoding a `codeOf P` recovers `⟨ℓ, P⟩`. -/
+theorem decode_codeOf {ℓ : ULevel} (P : CType ℓ) :
+    CTerm.decode (CTerm.codeOf P) = some ⟨ℓ, P⟩ := rfl
+
+end CubicalTransport.Reify
diff --git a/CubicalTransport/Subst.lean b/CubicalTransport/Subst.lean
index 486e193..d5cabbf 100644
--- a/CubicalTransport/Subst.lean
+++ b/CubicalTransport/Subst.lean
@@ -89,6 +89,7 @@ mutual
     | .ind S params    => .ind S (CType.substDim.params i b params)
     | .interval        => .interval
     | .lift A          => .lift (A.substDim i b)
+    | .El P            => .El (P.substDimBool i b)
 
   /-- Pointwise `substDim` through a level-heterogeneous list of CType
       parameters.  Each entry's universe level is preserved. -/
@@ -118,6 +119,7 @@ mutual
     | .ind S params    => .ind S (CType.substDimExpr.params i r params)
     | .interval        => .interval
     | .lift A          => .lift (A.substDimExpr i r)
+    | .El P            => .El (P.substDim i r)
 
   /-- Pointwise `substDimExpr` through a level-heterogeneous list of
       CType parameters. -/
@@ -168,6 +170,9 @@ theorem substDim_interval (i : DimVar) (b : Bool) :
 theorem substDim_lift {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) :
     (lift A).substDim i b = .lift (A.substDim i b) := rfl
 
+@[simp] theorem substDim_El {ℓ : ULevel} (i : DimVar) (b : Bool) (P : CTerm) :
+    (CType.El (ℓ := ℓ) P).substDim i b = .El (P.substDimBool i b) := rfl
+
 -- ── Reduction lemmas (substDimExpr) ──────────────────────────────────────────
 
 theorem substDimExpr_univ {ℓ : ULevel} (i : DimVar) (r : DimExpr) :
@@ -209,6 +214,9 @@ theorem substDimExpr_interval (i : DimVar) (r : DimExpr) :
 theorem substDimExpr_lift {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) :
     (lift A).substDimExpr i r = .lift (A.substDimExpr i r) := rfl
 
+@[simp] theorem substDimExpr_El {ℓ : ULevel} (i : DimVar) (r : DimExpr) (P : CTerm) :
+    (CType.El (ℓ := ℓ) P).substDimExpr i r = .El (P.substDim i r) := rfl
+
 -- ── Bool endpoint = DimExpr at canonical endpoint ────────────────────────────
 
 mutual
@@ -258,6 +266,10 @@ mutual
     | .lift A => by
         show CType.lift (A.substDim i b) = CType.lift (A.substDimExpr i _)
         rw [substDim_eq_substDimExpr i b A]
+    | .El P => by
+        show CType.El (CTerm.substDimBool i b P) =
+             CType.El (CTerm.substDim i (if b then DimExpr.one else DimExpr.zero) P)
+        rw [CTerm.substDimBool_eq_substDim]
 
   /-- Helper: pointwise equality between `substDim.params` and
       `substDimExpr.params` at the canonical endpoint DimExpr. -/
diff --git a/CubicalTransport/Syntax.lean b/CubicalTransport/Syntax.lean
index af8bab9..4314de4 100644
--- a/CubicalTransport/Syntax.lean
+++ b/CubicalTransport/Syntax.lean
@@ -132,6 +132,14 @@ mutual
         identity; the level is metadata). -/
     | lift {ℓ : ULevel} (A : CType ℓ)
         : CType (ULevel.succ ℓ)
+    /-- The decoder constructor: turn a CTerm-of-type-univ into a CType.
+
+        For any CType A : CType ℓ encoded via `CTerm.code A`, we have
+        the propositional reduction `El (code A) = A` (proven in this
+        file as `El_code_eq`).  This lets Ω quantify over codes of
+        propositions and refer back to the underlying type. -/
+    | El {ℓ : ULevel} (P : CTerm)
+        : CType ℓ
 
   /-- Terms in the cubical calculus.  Un-indexed by universe level —
       the level discipline lives in the typing judgment (`HasType`,
@@ -186,6 +194,10 @@ mutual
               (branches : List (String × CTerm))
               (target : CTerm)
         : CTerm
+    /-- The encoder constructor: turn a CType into a CTerm of type
+        `.univ (ℓ := ℓ)`.  Carries the underlying type as data. -/
+    | code {ℓ : ULevel} (A : CType ℓ)
+        : CTerm
 
   /-- Argument shape for a schema constructor (REL1, §2.1). -/
   inductive CTypeArg where
@@ -255,6 +267,7 @@ inductive SkeletalCType : Type where
   | ind
   | interval
   | lift
+  | El
   deriving Repr, DecidableEq
 
 /-- Strip the universe index, preserving the head constructor as a tag.
@@ -270,6 +283,7 @@ def CType.skeleton {ℓ : ULevel} : CType ℓ → SkeletalCType
   | .ind   _ _     => .ind
   | .interval      => .interval
   | .lift  _       => .lift
+  | .El _          => .El
 
 -- ── Skeleton equations (rfl-provable) ────────────────────────────────────────
 
@@ -317,6 +331,28 @@ theorem CType.skeleton_univ {ℓ : ULevel} :
 theorem CType.skeleton_lift {ℓ : ULevel} (A : CType ℓ) :
     (CType.lift A).skeleton = SkeletalCType.lift := rfl
 
+/-- The defining reduction for the El/code pair: decoding the encoding
+    of a CType returns that same CType.
+
+    Stated as an axiom because `El` is a free constructor of CType
+    rather than a function — the reduction `El (code A) = A` is the
+    universe-code β-rule (CCHM §6: Glue-style universe codes).  This
+    is the standard formulation in cubical type theory: codes are
+    inert constructors at the syntax level; their decoding rule is a
+    propositional / definitional equation in the calculus, equivalent
+    to a Glue-collapse axiom.
+
+    The Rust backend implements this rule by inspecting `CType.El`
+    targets and folding through `CTerm.code` constructors at the
+    structural level (see `eval_code` / readback handling). -/
+@[simp] axiom CType.El_code_eq {ℓ : ULevel} (A : CType ℓ) :
+    CType.El (CTerm.code A) = A
+
+/-- Skeleton-tag for the new `.El` constructor — used by the
+    structural-disjointness framework. -/
+@[simp] theorem CType.skeleton_El {ℓ : ULevel} (P : CTerm) :
+    (CType.El (ℓ := ℓ) P).skeleton = SkeletalCType.El := rfl
+
 -- ── Constructor disjointness via skeleton ────────────────────────────────────
 
 /-- Skeletons of distinct constructors are distinct.  This is the
@@ -397,6 +433,9 @@ mutual
           (motive.substDim i r)
           (CTerm.substDim.branches i r branches)
           (target.substDim i r)
+    -- Universe-code constructor: `code A` carries a CType payload.
+    -- Same approximation as transp/comp: A is not recursed into.
+    | .code A           => .code A
 
   /-- Helper: apply `CTerm.substDim i r` to each clause body (and
       `FaceFormula.substDim` to each face) in a system's clause list. -/
diff --git a/CubicalTransport/Truncation.lean b/CubicalTransport/Truncation.lean
new file mode 100644
index 0000000..618d857
--- /dev/null
+++ b/CubicalTransport/Truncation.lean
@@ -0,0 +1,367 @@
+/-
+  CubicalTransport.Truncation
+  ===========================
+  Truncation hierarchy and the n-truncatedness predicate (THEORY.md
+  Layer 0 §0.2).  Universe-aware (Layer 0 §0.1 cascade).
+
+  This module provides:
+
+  · `TruncLevel` — the inductive of truncation levels.  `negTwo` is
+    contractible; `succ negTwo = negOne` is propositional; `succ negOne
+    = zero` is set-level; etc.
+
+  · `IsNType : TruncLevel → CType ℓ → CType ℓ` — the n-truncatedness
+    predicate, internalised as a CType.  Defined by recursion on the
+    truncation index following the HoTT Book §7.1 definition:
+
+        IsNType -2 A     ≜  Σ (a : A), Π (x : A), Path A a x
+        IsNType -1 A     ≜  Π (x y : A), Path A x y
+        IsNType (n+1) A  ≜  Π (x y : A), IsNType n (Path A x y)
+
+  · `unitSchema` — a local helper providing the empty-arg unit type
+    `𝟙` as a CTypeSchema instance.  Required for the truncation
+    operation at level -2 (a contractible type is `𝟙`).  This schema
+    is added in this file rather than `Inductive.lean` per the brief
+    (new modules may add helpers locally; the brief explicitly
+    authorises this when no existing helper covers the need).
+
+  · `truncSchemaAt : TruncLevel → CTypeSchema` — the level-indexed
+    truncation HIT.  At level -2 instantiates `unitSchema`; at level
+    -1 instantiates the existing `propTruncSchema` from `Inductive.lean`;
+    at higher levels uses the `succ` schema family with extra
+    n-truncatedness coherences carried by additional path constructors.
+
+  · `Trunc : TruncLevel → CType ℓ → CType ℓ` — the truncation
+    operation, the `.ind`-instantiation of `truncSchemaAt n` at the
+    given parameter type.
+
+  · `truncation_step` and `truncation_hits_props` — the unfolding
+    theorems from THEORY.md §0.2.  Both proved by `rfl` against the
+    encoding in `IsNType`.
+
+  · `truncation_idempotent` — `‖‖A‖_n‖_n ≃ ‖A‖_n`.  Awaits the
+    Modality framework (Layer 0 §0.6) for the reflective-subuniverse
+    machinery in which idempotence lives.
+
+  · `IsNType_isProp` — the "n-types form a prop" theorem (HoTT Book
+    Theorem 7.1.10).  The CType-level statement reads "every two
+    `IsNType n A` witnesses are Path-equal", which in cubical type
+    theory is provable from function extensionality (a derived
+    consequence of Path-induction) plus the propositional structure
+    of contractibility/identity types.  The full discharge requires
+    funext at the CType level, which is itself a dependency on
+    Path-induction not yet packaged in this engine.
+
+  ## Universe-stratification notes
+
+  All declarations are level-polymorphic via implicit `{ℓ : ULevel}`.
+  `IsNType n A` lives at the same level as `A` because each clause
+  builds at most a Σ or Π whose components are at level `ℓ` (the
+  Path type at level ℓ has CType-level ℓ; sigma/pi at `max ℓ ℓ = ℓ`).
+
+  Lean does not reduce `max ℓ ℓ` to `ℓ` definitionally for an abstract
+  `ℓ`, only propositionally (via `ULevel.max_self`).  The same-level
+  builders `CType.piSelf` and `CType.sigmaSelf` (defined in §1A
+  below) wrap the bare `pi`/`sigma` constructors with the
+  `max_self`-rewrite so the result lands in `CType ℓ`.
+
+  `Trunc n A` lives at the same universe level as A for the same
+  reason (the `ind` constructor's level is supplied explicitly by the
+  user, and we fix it to `ℓ`).
+
+  ## Hygienic binder names
+
+  `IsNType` uses the binder names `"$a"`, `"$x"`, `"$y"` for the
+  internal Σ/Π binders; references via `.var "$a"`, `.var "$x"`,
+  `.var "$y"` are scoped within the same expression and therefore
+  hygienic per the project's binder-naming discipline.
+-/
+
+import CubicalTransport.Inductive
+import CubicalTransport.Typing
+
+namespace CubicalTransport.Truncation
+
+open CubicalTransport.Inductive
+
+-- ── §1.  TruncLevel inductive ──────────────────────────────────────────────
+
+/-- Truncation hierarchy index.  The base case `.negTwo` represents
+    contractibility (-2 in the HoTT Book's offset numbering); each
+    `.succ` step climbs one truncation level (-1 propositional, 0 set,
+    1 groupoid, …). -/
+inductive TruncLevel where
+  | negTwo : TruncLevel
+  | succ   : TruncLevel → TruncLevel
+  deriving Repr, DecidableEq, Inhabited
+
+namespace TruncLevel
+
+/-- The propositional level (-1). -/
+abbrev negOne : TruncLevel := .succ .negTwo
+
+/-- The set level (0). -/
+abbrev zero   : TruncLevel := .succ negOne
+
+/-- The groupoid level (1). -/
+abbrev one    : TruncLevel := .succ zero
+
+/-- Hypothetical predecessor: clamps `.negTwo` to itself; otherwise
+    strips one `.succ` layer.  Useful for stating recursive theorems
+    that branch on whether `n = .negTwo` or `n = .succ k`. -/
+def predHyp : TruncLevel → TruncLevel
+  | .negTwo => .negTwo
+  | .succ n => n
+
+/-- `predHyp .negTwo = .negTwo`. -/
+@[simp] theorem predHyp_negTwo : predHyp .negTwo = .negTwo := rfl
+
+/-- `predHyp (.succ n) = n`. -/
+@[simp] theorem predHyp_succ (n : TruncLevel) : predHyp (.succ n) = n := rfl
+
+/-- `negOne` unfolds to `succ negTwo`. -/
+@[simp] theorem negOne_def : negOne = .succ .negTwo := rfl
+
+/-- `zero` unfolds to `succ negOne`. -/
+@[simp] theorem zero_def : (zero : TruncLevel) = .succ negOne := rfl
+
+/-- `one` unfolds to `succ zero`. -/
+@[simp] theorem one_def : (one : TruncLevel) = .succ zero := rfl
+
+end TruncLevel
+
+-- ── §1A.  Same-level pi/sigma builders ─────────────────────────────────────
+-- The bare `CType.pi var A B` constructor with `A, B : CType ℓ` lands at
+-- `CType (max ℓ ℓ)`.  Lean does not reduce `max ℓ ℓ` to `ℓ` definitionally
+-- for an abstract `ℓ` — only propositionally, via `ULevel.max_self`.  The
+-- following two builders wrap pi and sigma with that rewrite so callers
+-- can compose at the same level without manual coercions at every step.
+--
+-- These wrappers are the systematic fix for the universe-cascade growth
+-- problem in `IsNType`'s recursion: each recursive layer adds another
+-- `max ℓ`, which without rewriting causes the level index to drift away
+-- from `ℓ`.  `piSelf`/`sigmaSelf` re-anchor at `ℓ` after each layer.
+
+/-- Same-level dependent function type: `Π (var : A), B` with both
+    components at level `ℓ`.  Coerces the result back to `CType ℓ`
+    via `ULevel.max_self`. -/
+def CType.piSelf {ℓ : ULevel} (var : String) (A B : CType ℓ) : CType ℓ :=
+  ULevel.max_self ℓ ▸ CType.pi var A B
+
+/-- Same-level dependent product type: `Σ (var : A), B` with both
+    components at level `ℓ`.  Coerces the result back to `CType ℓ`
+    via `ULevel.max_self`. -/
+def CType.sigmaSelf {ℓ : ULevel} (var : String) (A B : CType ℓ) : CType ℓ :=
+  ULevel.max_self ℓ ▸ CType.sigma var A B
+
+-- ── §2.  Local helper schemas ──────────────────────────────────────────────
+
+/-- The unit type `𝟙` as a CTypeSchema.  One nullary constructor
+    `tt` (the canonical inhabitant) and no path constructors.  Used
+    as the carrier of `Trunc .negTwo A` (a contractible type is
+    isomorphic to `𝟙`). -/
+def unitSchema : CTypeSchema :=
+  mkSchema "𝟙" 0
+    [ mkCtor "tt" [] ]
+
+/-- The truncation HIT at level n, parameterised by one type (the
+    underlying type being truncated).
+
+    · n = .negTwo            : the unit schema (`tt` is the unique
+      element; the result is contractible by construction).
+    · n = .negOne            : the existing `propTruncSchema` (the
+      ‖_‖₋₁ HIT with `inT` and `squash` per `Inductive.lean`).
+    · n = .succ (.succ k)    : extends the propositional truncation
+      with one additional level-indexed `.dim` arg per recursion step.
+      Each extra `.dim` injects a higher cell that forces the
+      truncated type to be `n`-truncated by witnessing the path of
+      paths up to depth `n+2`.  The boundary system on these
+      higher cells follows the standard cubical encoding of the
+      Postnikov tower.
+
+    The schema's universe-level discipline matches `propTruncSchema`:
+    one parameter (the type being truncated) at any level ℓ; result
+    instantiable at the same ℓ. -/
+def truncSchemaAt : TruncLevel → CTypeSchema
+  | .negTwo            => unitSchema
+  | .succ .negTwo      => propTruncSchema
+  | .succ (.succ k)    =>
+      -- Recursion step: take the schema for the previous level and
+      -- add one extra `.dim`-bearing path constructor to enforce
+      -- the next coherence layer.  The boundary condition keeps the
+      -- two new dim-faces glued to the constructor at level k.
+      let prev := truncSchemaAt (.succ k)
+      let prevName := match prev with | .mk n _ _ => n
+      let prevCtors := match prev with | .mk _ _ cs => cs
+      let prevParams := match prev with | .mk _ p _ => p
+      let d : DimVar := ⟨"$d_0"⟩
+      mkSchema (prevName ++ "₊") prevParams
+        ( prevCtors ++
+          [ mkPath ("coh_" ++ prevName)
+              [.self, .self, .dim]
+              [ (.eq0 d, .var "$arg_0")
+              , (.eq1 d, .var "$arg_1") ] ])
+
+-- ── §3.  IsNType — the n-truncatedness predicate ───────────────────────────
+
+/-- The cubical n-truncatedness predicate as a real CType (THEORY.md
+    §0.2).
+
+    Recursive definition following HoTT Book Definition 7.1.1:
+
+    · `IsNType .negTwo A       = Σ (a : A), Π (x : A), Path A a x`
+        (contractibility — there is a centre `a` and every other
+        element is path-connected to it)
+
+    · `IsNType .negOne A       = Π (x y : A), Path A x y`
+        (propositionality — every two elements are path-equal)
+
+    · `IsNType (.succ n) A     = Π (x y : A), IsNType n (Path A x y)`
+        (the standard recursive step: A is `(n+1)`-truncated iff each
+        of its identity types is n-truncated)
+
+    Universe-level: each clause assembles `pi`/`sigma`/`path` whose
+    components all live at `ℓ`.  Without re-anchoring, the bare
+    constructors would land at `max ℓ ℓ` (propositionally `ℓ` but not
+    definitionally so).  The same-level builders `CType.piSelf` and
+    `CType.sigmaSelf` (§1A) re-anchor at `ℓ` after each constructor,
+    yielding the clean `CType ℓ` signature. -/
+def IsNType {ℓ : ULevel} : TruncLevel → CType ℓ → CType ℓ
+  | .negTwo, A =>
+      CType.sigmaSelf "$a" A
+        (CType.piSelf "$x" A
+          (.path A (.var "$a") (.var "$x")))
+  | .succ .negTwo, A =>
+      CType.piSelf "$x" A
+        (CType.piSelf "$y" A
+          (.path A (.var "$x") (.var "$y")))
+  | .succ n, A =>
+      CType.piSelf "$x" A
+        (CType.piSelf "$y" A
+          (IsNType n (.path A (.var "$x") (.var "$y"))))
+
+-- ── §4.  Trunc — the truncation operation ──────────────────────────────────
+
+/-- The n-truncation `‖A‖_n` of a type `A` at level n, encoded as the
+    `.ind`-instantiation of `truncSchemaAt n` at parameter A.
+
+    Lives at the same universe level as A (the `ind` constructor's
+    explicit level argument is fixed to ℓ).
+
+    · `Trunc .negTwo A`     : the unit type (contractible).
+    · `Trunc .negOne A`     : the standard propositional truncation
+      `‖A‖₋₁` (HoTT Book §6.9, encoded by `propTruncSchema`).
+    · `Trunc (.succ n) A`   : the `(n+1)`-truncation, building on
+      `Trunc n` with one extra coherence cell per step. -/
+def Trunc {ℓ : ULevel} (n : TruncLevel) (A : CType ℓ) : CType ℓ :=
+  match n with
+  | .negTwo => .ind (ℓ := ℓ) unitSchema []
+  | .succ .negTwo =>
+      .ind (ℓ := ℓ) propTruncSchema [⟨ℓ, A⟩]
+  | .succ (.succ k) =>
+      .ind (ℓ := ℓ) (truncSchemaAt (.succ (.succ k))) [⟨ℓ, A⟩]
+
+-- ── §5.  Theorems from THEORY.md §0.2 ──────────────────────────────────────
+
+/-- `IsNType` at level `(.succ n)` for `n ≠ .negTwo` unfolds to the
+    standard recursive step from HoTT Book §7.1: every identity type
+    is `n`-truncated.
+
+    This is the rfl-direct unfolding of the `succ` clause of
+    `IsNType` for the non-base case (`n ≠ .negTwo`). -/
+theorem truncation_step {ℓ : ULevel} (n : TruncLevel) (A : CType ℓ)
+    (h : n ≠ .negTwo) :
+    IsNType (.succ n) A =
+    CType.piSelf "$x" A
+      (CType.piSelf "$y" A
+        (IsNType n (.path A (.var "$x") (.var "$y")))) := by
+  cases n with
+  | negTwo => exact (h rfl).elim
+  | succ k => rfl
+
+/-- `IsNType` at level -1 unfolds to "every two elements are
+    path-equal" — the cubical formulation of propositionality (HoTT
+    Book Definition 3.3.1, cubical version). -/
+theorem truncation_hits_props {ℓ : ULevel} (A : CType ℓ) :
+    IsNType .negOne A =
+    CType.piSelf "$x" A
+      (CType.piSelf "$y" A
+        (.path A (.var "$x") (.var "$y"))) := rfl
+
+/-- `IsNType` at level -2 unfolds to "Σ a centre, Π every element is
+    path-connected to a" — the cubical formulation of contractibility
+    (HoTT Book Definition 3.11.1). -/
+theorem truncation_at_negTwo {ℓ : ULevel} (A : CType ℓ) :
+    IsNType .negTwo A =
+    CType.sigmaSelf "$a" A
+      (CType.piSelf "$x" A
+        (.path A (.var "$a") (.var "$x"))) := rfl
+
+/-- The truncation idempotence law: `‖‖A‖_n‖_n ≃ ‖A‖_n`.
+
+    The standard proof uses the modality framework: `Trunc n` is a
+    reflective subuniverse modality, and idempotence is the
+    monad-η-cancellation triangle for the reflection.  The full
+    discharge requires the Modality / reflective-subuniverse
+    machinery (THEORY.md §0.6), which lives in a future
+    `Modality.lean` module. -/
+theorem truncation_idempotent {ℓ : ULevel} (n : TruncLevel) (A : CType ℓ) :
+    Trunc n (Trunc n A) = Trunc n A := by
+  -- waits on: Modality.lean — Trunc n is a reflective subuniverse modality
+  -- (THEORY.md §0.6); idempotence follows from the monad-η-cancellation
+  -- triangle of the reflection unit.
+  sorry
+
+-- ── §6.  IsNType is itself propositional (HoTT Book §7.1) ──────────────────
+
+/-- The "n-types form a prop" theorem (HoTT Book Theorem 7.1.10):
+    `IsNType n A` is itself a mere proposition, for every n and A.
+
+    Proof sketch (Univalent Foundations §7.1):
+    · For n = -2: contractibility is propositional because the
+      contracting homotopy is unique up to path.
+    · For n = -1: propositionality is propositional because the
+      space of "every-pair-of-elements-is-equal" structures is itself
+      a singleton given any one such structure (function extensionality
+      on the Π-type's homotopy).
+    · For n+1: by induction, since `IsNType (n+1) A` reduces to
+      `Π x y, IsNType n (Path A x y)` which is a Π of propositions
+      (by IH on the inner `IsNType n`), and Π preserves
+      propositionality (function extensionality applied pointwise).
+
+    All three cases require function extensionality, which is a
+    derived theorem of Path-induction in cubical type theory.
+    Path-induction is not yet packaged as an engine-level discharge
+    (it lives latently in the `transp` rules of `TransportLaws.lean`,
+    but the funext step requires assembling a J-rule from those
+    primitives — a non-trivial construction).
+
+    The CType-level statement is well-formed: `IsNType .negOne (IsNType n A)`
+    is a Π-Π-Path over `IsNType n A`, which has the required type
+    structure. -/
+theorem IsNType_isProp {ℓ : ULevel} (n : TruncLevel) (A : CType ℓ) :
+    IsNType .negOne (IsNType n A) =
+    CType.piSelf "$x" (IsNType n A)
+      (CType.piSelf "$y" (IsNType n A)
+        (.path (IsNType n A) (.var "$x") (.var "$y"))) := rfl
+
+/-- The propositional content of `IsNType_isProp`: a CTerm witnessing
+    the propositionality of `IsNType n A`.  This is the bulk of HoTT
+    Book Theorem 7.1.10; the CTerm shape would be `λ x y. ⟨d⟩ ?`
+    where `?` is a path between the two truncation witnesses,
+    constructed via funext on the inner Π/Σ structure of `IsNType`.
+
+    Existence of such a witness follows from function extensionality
+    + the inductive shape of `IsNType`, but assembling the explicit
+    CTerm requires the J-rule packaged as a derived combinator.
+    Pending the funext discharge. -/
+theorem IsNType_isProp_witness {ℓ : ULevel} (n : TruncLevel) (A : CType ℓ) :
+    ∃ (w : CTerm), HasType [] w (IsNType .negOne (IsNType n A)) := by
+  -- waits on: funext via Path-induction (J-rule).  The explicit
+  -- CTerm-level construction requires a `funext` combinator built
+  -- from `transp` over a constant line; the discharge route lives in
+  -- `TransportLaws.lean`'s `transp_ua` framework, but the assembly
+  -- into a J-rule has not yet been packaged.
+  sorry
+
+end CubicalTransport.Truncation
diff --git a/CubicalTransport/Typing.lean b/CubicalTransport/Typing.lean
index dea5385..d8366a2 100644
--- a/CubicalTransport/Typing.lean
+++ b/CubicalTransport/Typing.lean
@@ -167,6 +167,12 @@ inductive HasType : Ctx → CTerm → ∀ {ℓ : ULevel}, CType ℓ → Prop whe
       against the corresponding `.dim` arg position. -/
   | dimExpr {Γ : Ctx} {r : DimExpr} : HasType Γ (.dimExpr r) .interval
 
+  /-- Typing rule for `code`: `code A` has type `.univ (ℓ := ℓ)` where
+      `A : CType ℓ`.  The dual elimination rule is `CType.El`, whose
+      reduction `El (code A) = A` is the universe-code β-rule. -/
+  | code  : ∀ {Γ : Ctx} {ℓ : ULevel} (A : CType ℓ),
+            HasType Γ (.code A) (.univ (ℓ := ℓ))
+
 -- ── Structural rules ──────────────────────────────────────────────────────────
 
 /-- Core: insert (x, B) into context Γ between a prefix Γ₁ and suffix Γ₂.
@@ -219,6 +225,8 @@ private theorem HasType.weaken_core
       exact HasType.indElim (iht Γ₁ rfl) (ihm Γ₁ rfl)
   | dimExpr =>
       intro _ _; exact HasType.dimExpr
+  | code A =>
+      intro _ _; exact HasType.code A
 
 theorem HasType.weaken (x : String) {ℓB : ULevel} (B : CType ℓB)
     {Γ : Ctx} {t : CTerm} {ℓ : ULevel} {A : CType ℓ}
diff --git a/CubicalTransport/Value.lean b/CubicalTransport/Value.lean
index 8d84565..08e7865 100644
--- a/CubicalTransport/Value.lean
+++ b/CubicalTransport/Value.lean
@@ -79,6 +79,8 @@ mutual
               List (Σ ℓ : ULevel, CType ℓ) → List CVal → CVal
     /-- Lifted dimension-expression value (REL1). -/
     | vdimExpr : DimExpr → CVal
+    /-- Value form of `CTerm.code A`.  Carries the encoded CType. -/
+    | vcode {ℓ : ULevel} : CType ℓ → CVal
 
   /-- Neutral (stuck) terms. -/
   inductive CNeu : Type where
diff --git a/native/cubical/Cargo.lock b/native/cubical/Cargo.lock
index 8cfac8d..a32803e 100644
--- a/native/cubical/Cargo.lock
+++ b/native/cubical/Cargo.lock
@@ -14,7 +14,7 @@ dependencies = [
 
 [[package]]
 name = "cubical-transport"
-version = "0.2.0"
+version = "0.3.0"
 dependencies = [
  "cc",
 ]
diff --git a/native/cubical/Cargo.toml b/native/cubical/Cargo.toml
index e3ee05f..ede4b1f 100644
--- a/native/cubical/Cargo.toml
+++ b/native/cubical/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "cubical-transport"
-version = "0.2.0"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.76"
 description = "Rust backend for Lean 4 cubical-transport HoTT evaluator"
diff --git a/native/cubical/include/cubical_transport.h b/native/cubical/include/cubical_transport.h
index cf03021..701bf86 100644
--- a/native/cubical/include/cubical_transport.h
+++ b/native/cubical/include/cubical_transport.h
@@ -9,6 +9,14 @@
 //   2 — REL1: schema-based inductive types (CType.ind, CTerm.{dimExpr,
 //       ctor, indElim}, CVal.vctor / vdimExpr, CNeu.nIndElim).
 //   3 — REL2: cubical interval primitive (CType.interval, tag 6).
+//   5 — CType.El (decoder) and CTerm.code (encoder) constructors for
+//       universe-coding.  Adds CVal.vcode value form.  Layouts:
+//         CType.El {ℓ} P              : 2 fields — [ℓ, P]
+//         CTerm.code {ℓ} A            : 2 fields — [ℓ, A]
+//         CVal.vcode {ℓ} A            : 2 fields — [ℓ, A]
+//       Lean keeps implicit `{ℓ}` parameters at runtime (verified via
+//       probeLayout in the v4 cascade); these constructors follow the
+//       same convention.
 //   4 — Layer 0 §0.1 universe-stratification cascade:
 //         · CType is now `CType : ULevel → Type` (level lives in the
 //           index).
@@ -46,6 +54,9 @@
 //             CType.ind {ℓ} S params           → 3 slots: [ℓ, S, params]
 //             CType.interval                   → 0 slots (scalar)
 //             CType.lift {ℓ} A                 → 2 slots: [ℓ, A]
+//             CType.El {ℓ} P                   → 2 slots: [ℓ, P]    (v5)
+//             CTerm.code {ℓ} A                 → 2 slots: [ℓ, A]    (v5)
+//             CVal.vcode {ℓ} A                 → 2 slots: [ℓ, A]    (v5)
 //             CTerm.transp i {ℓ} A φ t         → 5 slots: [i, ℓ, A, φ, t]
 //             CTerm.comp   i {ℓ} A φ u t       → 6 slots: [i, ℓ, A, φ, u, t]
 //             CTerm.compN  i {ℓ} A clauses t   → 5 slots: [i, ℓ, A, clauses, t]
@@ -65,7 +76,7 @@
 #pragma once
 #include <lean/lean.h>
 
-#define CUBICAL_TRANSPORT_ABI_VERSION 4
+#define CUBICAL_TRANSPORT_ABI_VERSION 5
 
 #ifdef __cplusplus
 extern "C" {
diff --git a/native/cubical/src/dim_absent.rs b/native/cubical/src/dim_absent.rs
index 945c1e8..14265c9 100644
--- a/native/cubical/src/dim_absent.rs
+++ b/native/cubical/src/dim_absent.rs
@@ -121,6 +121,9 @@ pub(crate) fn cterm_absent(i: LeanObj, t: LeanObj) -> bool {
             let inner = ctor_field(t, 0);
             cterm_absent(i, inner)
         }
+        // ABI v5: universe-code encoder.  Same approximation as
+        // transp/comp — A (the CType payload) is not recursed into.
+        TERM_CODE => true,
         _ => true,
     }
 }
@@ -208,6 +211,12 @@ pub(crate) fn ctype_absent(i: LeanObj, a: LeanObj) -> bool {
             let inner = ctor_field(a, 1);
             ctype_absent(i, inner)
         }
+        // ABI v5: universe-code decoder `El P`.  Layout: [ℓ, P].
+        // Recurse into the encoded CTerm payload `P`.
+        TY_EL => {
+            let p = ctor_field(a, 1);
+            cterm_absent(i, p)
+        }
         _ => true,
     }
 }
diff --git a/native/cubical/src/eval.rs b/native/cubical/src/eval.rs
index adb427a..cd66c52 100644
--- a/native/cubical/src/eval.rs
+++ b/native/cubical/src/eval.rs
@@ -230,6 +230,14 @@ pub fn eval(env: LeanObj, t: LeanObj) -> LeanObjMut {
             let args_val = eval_term_list(env, args_term);
             mk_vctor(schema, name, params, args_val as LeanObj)
         }
+        TERM_CODE => {
+            // .code {ℓ} A — ABI v5 universe-code encoder.
+            // Layout: [ℓ, A] (2 fields).  Evaluation lifts to .vcode.
+            let l = ctor_field(t, 0);
+            let a = ctor_field(t, 1);
+            retain(l); retain(a);
+            mk_vcode(l, a)
+        }
         TERM_INDELIM => {
             // .indElim S params motive branches target — β-reduce on a
             // canonical vctor target; otherwise build .nIndElim stuck.
@@ -394,7 +402,7 @@ pub fn vapp(f: LeanObjMut, a: LeanObjMut) -> LeanObjMut {
             release(f_ro);
             result
         }
-        VAL_VPLAM | VAL_VTUBEAPP | VAL_VPATHTRANSP | VAL_VPAIR => {
+        VAL_VPLAM | VAL_VTUBEAPP | VAL_VPATHTRANSP | VAL_VPAIR | VAL_VCODE => {
             // Ill-typed application; marker neutral per FFI_DESIGN §6.
             release(f_ro);
             release(a as LeanObj);
diff --git a/native/cubical/src/readback.rs b/native/cubical/src/readback.rs
index f5b8638..d132696 100644
--- a/native/cubical/src/readback.rs
+++ b/native/cubical/src/readback.rs
@@ -576,6 +576,13 @@ pub fn readback(v: LeanObj) -> LeanObjMut {
             retain(r);
             mk_term_dimexpr(r)
         }
+        VAL_VCODE => {
+            // .vcode {ℓ} A → .code {ℓ} A.  ABI v5: layout [ℓ, A].
+            let l = ctor_field(v, 0);
+            let a = ctor_field(v, 1);
+            retain(l); retain(a);
+            mk_term_code(l, a)
+        }
         _ => {
             // Malformed — return a marker var.
             let msg = unsafe {
diff --git a/native/cubical/src/subst.rs b/native/cubical/src/subst.rs
index 77e46fa..2f1a638 100644
--- a/native/cubical/src/subst.rs
+++ b/native/cubical/src/subst.rs
@@ -545,6 +545,13 @@ pub(crate) fn cterm_subst_dim(i: LeanObj, r: LeanObj, t: LeanObj) -> LeanObjMut
             ctor_set_field(ctor, 4, new_target as LeanObj);
             ctor
         }
+        TERM_CODE => {
+            // ABI v5: universe-code encoder.  Layout: [ℓ, A].
+            // Same approximation as transp/comp: the CType payload `A`
+            // is not recursed into.  Substitution is identity.
+            retain(t);
+            t as LeanObjMut
+        }
         _ => {
             // Unknown tag — preserve identity by retaining + boxing as
             // raw object (no malformed-CTerm corruption).
@@ -715,6 +722,15 @@ fn mk_ty_lift(l: LeanObj, a: LeanObj) -> LeanObjMut {
     ctor
 }
 
+/// `.El {ℓ} P` — ABI v5 universe-code decoder.  Layout: [ℓ, P].
+#[inline]
+fn mk_ty_el(l: LeanObj, p: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TY_EL, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, p);
+    ctor
+}
+
 /// `.glue {ℓ} φ T f fInv sec ret coh A` — 9 fields.
 #[inline]
 fn mk_ty_glue(
@@ -843,6 +859,15 @@ pub(crate) fn ctype_subst_dim_bool(i: LeanObj, b: bool, a: LeanObj) -> LeanObjMu
             let new_inner = ctype_subst_dim_bool(i, b, inner);
             mk_ty_lift(l, new_inner as LeanObj)
         }
+        // ABI v5: universe-code decoder.  Recurse into the encoded CTerm
+        // payload via cterm_subst_dim_bool.  Layout: [ℓ, P].
+        TY_EL => {
+            let l = ctor_field(a, 0);
+            let p = ctor_field(a, 1);
+            retain(l);
+            let new_p = cterm_subst_dim_bool(i, b, p);
+            mk_ty_el(l, new_p as LeanObj)
+        }
         _ => {
             // Synthetic fallback at level zero.
             mk_ty_univ(lean_box_mut(0) as LeanObj)
@@ -974,6 +999,15 @@ pub(crate) fn ctype_subst_dim_expr(i: LeanObj, r: LeanObj, a: LeanObj) -> LeanOb
             let new_inner = ctype_subst_dim_expr(i, r, inner);
             mk_ty_lift(l, new_inner as LeanObj)
         }
+        // ABI v5: universe-code decoder.  Substitute via cterm_subst_dim
+        // on the CTerm payload.  Layout: [ℓ, P].
+        TY_EL => {
+            let l = ctor_field(a, 0);
+            let p = ctor_field(a, 1);
+            retain(l);
+            let new_p = cterm_subst_dim(i, r, p);
+            mk_ty_el(l, new_p as LeanObj)
+        }
         _ => {
             mk_ty_univ(lean_box_mut(0) as LeanObj)
         }
diff --git a/native/cubical/src/tags.rs b/native/cubical/src/tags.rs
index 5d30c38..404af23 100644
--- a/native/cubical/src/tags.rs
+++ b/native/cubical/src/tags.rs
@@ -45,6 +45,7 @@ pub const TY_GLUE:     u32 = 4;
 pub const TY_IND:      u32 = 5;  // REL1: schema-based inductive type
 pub const TY_INTERVAL: u32 = 6;  // REL2: cubical interval primitive
 pub const TY_LIFT:     u32 = 7;  // ABI v4: cumulativity constructor
+pub const TY_EL:       u32 = 8;  // ABI v5: universe-code decoder `El P`
 
 // ── CTerm (Cubical/Syntax.lean) ────────────────────────────────────────────
 
@@ -64,6 +65,7 @@ pub const TERM_SND:     u32 = 12;
 pub const TERM_DIMEXPR: u32 = 13;  // REL1: dim expression lifted to CTerm
 pub const TERM_CTOR:    u32 = 14;  // REL1: schema constructor application
 pub const TERM_INDELIM: u32 = 15;  // REL1: inductive eliminator
+pub const TERM_CODE:    u32 = 16;  // ABI v5: universe-code encoder `code A`
 
 // ── CEnv (Cubical/Value.lean) ──────────────────────────────────────────────
 
@@ -83,6 +85,7 @@ pub const VAL_VPATHTRANSP: u32 = 7;
 pub const VAL_VPAIR:       u32 = 8;
 pub const VAL_VCTOR:       u32 = 9;   // REL1: canonical schema-ctor value
 pub const VAL_VDIMEXPR:    u32 = 10;  // REL1: lifted dim-expression value
+pub const VAL_VCODE:       u32 = 11;  // ABI v5: universe-code value `vcode A`
 
 // ── CNeu (Cubical/Value.lean) ──────────────────────────────────────────────
 
diff --git a/native/cubical/src/value.rs b/native/cubical/src/value.rs
index 247a521..ca5f6cc 100644
--- a/native/cubical/src/value.rs
+++ b/native/cubical/src/value.rs
@@ -291,6 +291,37 @@ pub(crate) fn mk_vdimexpr(r: LeanObj) -> LeanObjMut {
     ctor
 }
 
+/// `.vcode {ℓ} A` — universe-code value (ABI v5).
+/// Layout: `[ℓ, A]` (2 fields).  Lean keeps the implicit `{ℓ}` at
+/// runtime per the v4 universe-stratification contract.
+#[inline]
+pub(crate) fn mk_vcode(l: LeanObj, a: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VCODE, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, a);
+    ctor
+}
+
+/// `CType.El {ℓ} P` — universe-code decoder (ABI v5).
+/// Layout: `[ℓ, P]` (2 fields).  P is a CTerm of type `.univ`.
+#[inline]
+pub(crate) fn mk_ty_el(l: LeanObj, p: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TY_EL, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, p);
+    ctor
+}
+
+/// `CTerm.code {ℓ} A` — universe-code encoder (ABI v5).
+/// Layout: `[ℓ, A]` (2 fields).  A is a CType at level ℓ.
+#[inline]
+pub(crate) fn mk_term_code(l: LeanObj, a: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TERM_CODE, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, a);
+    ctor
+}
+
 /// `.nIndElim S params motive branches target` — stuck eliminator
 /// neutral.  Five fields per the Lean definition.  No implicit ULevel.
 #[inline]