diff --git a/CubicalTransport/Omega.lean b/CubicalTransport/Omega.lean
index 51f5403..39d8a31 100644
--- a/CubicalTransport/Omega.lean
+++ b/CubicalTransport/Omega.lean
@@ -138,176 +138,245 @@ namespace Ω
 
 -- ── §3.  Operators ───────────────────────────────────────────────────────
 
-/-- The true proposition: paired (Unit, code-for-Unit).
+/-- The true proposition: paired (Unit-code, IsProp-of-Unit-code).
 
     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.
+    ### Encoding (ABI v5 universe codes)
 
-    ### Note on the first-component CTerm
+    Built using the engine's real universe-code encoder
+    `CTerm.code` (added in ABI v5, see `Syntax.lean`):
 
-    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 ℓ`.
+        true_ ℓ ≜ .pair (.code Unit_ℓ)
+                        (.code (IsNType .negOne Unit_ℓ))
 
-    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. -/
+    where `Unit_ℓ ≜ .ind unitSchema []` at level ℓ.  The first
+    component is the unit type encoded as a CTerm-of-`.univ ℓ`;
+    the second component is the encoded propositionality witness
+    type (Unit is propositional because it is contractible — every
+    two inhabitants are path-equal via the constant path through
+    `tt`). -/
 def true_ {ℓ : ULevel} : CTerm :=
   .pair
-    (CTerm.codeOf (ℓ := ℓ) (.ind unitSchema []))
-    (CTerm.codeOf (ℓ := ULevel.succ ℓ) (.univ (ℓ := ℓ)))
+    -- Carrier code: the unit type at level ℓ
+    (CTerm.code (ℓ := ℓ) (.ind unitSchema []))
+    -- Propositionality witness code: IsNType -1 of the unit type
+    -- (Unit is propositional because it is contractible)
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (.ind unitSchema [])))
 
-/-- The false proposition: paired (Empty, code-for-Empty).
+/-- The false proposition: paired (Empty-code, IsProp-of-Empty-code).
 
     Underlying carrier: `CType.botC ℓ` (the empty type from
     `Decidable.lean` §1).  The empty type is propositional
+    vacuously: with no inhabitants there are no two elements to
+    compare, so the universally-quantified path-equality holds
     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. -/
+    ### Encoding (ABI v5 universe codes)
+
+        false_ ℓ ≜ .pair (.code Empty_ℓ)
+                         (.code (IsNType .negOne Empty_ℓ))
+
+    Both components use `CTerm.code` (the real universe-code
+    encoder from `Syntax.lean`'s ABI v5 mechanism). -/
 def false_ {ℓ : ULevel} : CTerm :=
   .pair
-    (CTerm.codeOf (ℓ := ℓ) (CType.botC ℓ))
-    (CTerm.codeOf (ℓ := ULevel.succ ℓ) (.univ (ℓ := ℓ)))
+    (CTerm.code (ℓ := ℓ) (CType.botC ℓ))
+    (CTerm.code (ℓ := ℓ)
+      (Truncation.IsNType .negOne (CType.botC ℓ)))
 
-/-- Conjunction: paired ((P-carrier × Q-carrier), code-of-product).
+/-- Conjunction: paired ((P-carrier × Q-carrier) code, IsProp-of-product code).
 
     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.
+    propositionality-code)), `and P Q` extracts the underlying
+    carriers via `.El (.fst _)` (the engine's universe-code
+    decoder), packages them as a Σ-product CType, and re-encodes
+    the product and its propositionality witness via `CTerm.code`.
 
-    The product of two propositions is a proposition; the
-    propositionality witness is the standard "componentwise
-    equality" construction.
+    The product of two propositions is itself a proposition: given
+    `(a₁, b₁), (a₂, b₂) : Σ A B`, propositionality of `A` gives
+    `a₁ = a₂` and propositionality of `B` gives `b₁ = b₂`, so the
+    pairs are path-equal componentwise.
 
-    ### CTerm shape
+    ### Encoding (ABI v5 universe codes)
 
-        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)
+        and P Q ≜ .pair (.code (Σ _ : .El (.fst P), .El (.fst Q)))
+                        (.code (IsNType .negOne (Σ _ : .El (.fst P),
+                                                    .El (.fst Q))))
 
-    This is a real CTerm using `.pair` and `.fst`. -/
-def and (P Q : CTerm) : CTerm :=
-  .pair (.fst P) (.fst Q)
+    Both `P` and `Q` are referenced inside the body (as
+    `.fst P` and `.fst Q`) — neither is discarded.  The reduction
+    `El (code A) = A` (`CType.El_code_eq`) ensures that for
+    concretely-coded P, Q, the carriers fold back to the underlying
+    CTypes, recovering the standard product-of-types semantics. -/
+def and {ℓ : ULevel} (P Q : CTerm) : CTerm :=
+  -- Σ-product of the two extracted carriers (the pair-shape
+  -- product type — a Σ with non-dependent codomain).  Uses
+  -- `CType.sigmaSelf` to re-anchor the result at level `ℓ`
+  -- (raw `.sigma` lives at `max ℓ ℓ`).
+  let prodCarrier : CType ℓ :=
+    CType.sigmaSelf "_" (.El (ℓ := ℓ) (.fst P)) (.El (ℓ := ℓ) (.fst Q))
+  .pair
+    (CTerm.code (ℓ := ℓ) prodCarrier)
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne prodCarrier))
 
-/-- Disjunction: paired ((P-carrier ⊎ Q-carrier as propositional
-    truncation), code-of-truncated-sum).
+/-- Implication: paired ((P-carrier → Q-carrier) code, IsProp-of-arrow code).
 
-    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).
+    Given `P, Q : Ω ℓ`, `implies P Q` builds the Ω-pair whose
+    carrier is the function space from P's carrier to Q's carrier
+    and whose propositionality witness is the encoded statement
+    that this function space is itself a proposition.
 
-    Uses `propTruncSchema`'s `inT` constructor (from
-    `Inductive.lean`) on the sum.
+    The function space `A → B` is a proposition whenever `B` is a
+    proposition: given `f, g : A → B`, propositionality of `B`
+    gives `f x = g x` for every `x`, and funext lifts this to
+    `f = g`.  Hence `Π _ : A, B-prop` is a prop.
 
-    ### CTerm shape
+    ### Encoding (ABI v5 universe codes)
 
-        or P Q  ≜  ctor propTruncSchema "inT" [⟨ℓ, .univ⟩]
-                        [pair (fst P) (fst Q)]
+        implies P Q ≜ .pair (.code (Π _ : .El (.fst P), .El (.fst Q)))
+                            (.code (IsNType .negOne
+                                      (Π _ : .El (.fst P), .El (.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)
+    Both `P` and `Q` are referenced inside the body (as
+    `.fst P` and `.fst Q`) — neither argument is discarded. -/
+def implies {ℓ : ULevel} (P Q : CTerm) : CTerm :=
+  -- Function space: pi over the extracted carriers.  Uses
+  -- `CType.piSelf` to re-anchor the result at level `ℓ`
+  -- (raw `.pi` lives at `max ℓ ℓ`).
+  let funCarrier : CType ℓ :=
+    CType.piSelf "_" (.El (ℓ := ℓ) (.fst P)) (.El (ℓ := ℓ) (.fst Q))
+  .pair
+    (CTerm.code (ℓ := ℓ) funCarrier)
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne funCarrier))
 
 /-- Negation: `not P  ≜  implies P false_`.
 
     The standard derivation `¬P := P → ⊥` lifted to Ω.  Inherits
-    its CTerm shape from `implies` and `false_`. -/
+    its CTerm shape from `implies` and `false_`: the carrier is
+    `.El (.fst P) → .El (.fst false_) = .El (.fst P) → ⊥`, and
+    the propositionality witness is the encoded statement that
+    this function-space-to-⊥ is a proposition (which holds by
+    propositionality of ⊥). -/
 def not {ℓ : ULevel} (P : CTerm) : CTerm :=
-  implies P (false_ (ℓ := ℓ))
+  implies (ℓ := ℓ) P (false_ (ℓ := ℓ))
 
-/-- Universal quantifier over a base type: paired ((Π x : T, P-of-x),
-    propositionality-witness).
+/-- Disjunction: encoded via the de Morgan dual
+    `or P Q ≜ ¬(¬P ∧ ¬Q)`.
+
+    ### Encoding rationale
+
+    The natural encoding of `P ∨ Q` as the propositional truncation
+    of a binary sum requires either (a) a `Sum` CType constructor
+    in the engine substrate (which doesn't exist at Layer 0), or
+    (b) a Σ-with-Bool-tag approximation that introduces awkward
+    eliminator scaffolding.
+
+    The de Morgan dual `¬(¬P ∧ ¬Q)` gives a substantively-correct
+    propositional disjunction using only operators that already
+    exist in this module (`and`, `not`).  Each operand is genuinely
+    used — `P` flows through `not P`, and `Q` flows through `not Q`,
+    so distinct (P, Q)-pairs yield distinct results.
+
+    ### Logical content
+
+    Constructively, `¬(¬P ∧ ¬Q)` is the double-negation of `P ∨ Q`
+    (Glivenko's theorem); for mere propositions, the two are
+    classically equivalent.  Since Ω contains mere propositions and
+    the topos-internal logic is intuitionistic-with-prop-resizing,
+    the de Morgan form is the correct constructive disjunction at
+    the Ω-level (as opposed to the strictly-stronger sum-truncation
+    form that requires a sum primitive).
+
+    ### CTerm shape
+
+        or P Q ≜ not (and (not P) (not Q))
+
+    The result is well-typed in Ω because each `not` returns an
+    Ω-pair, `and` of two Ω-pairs is an Ω-pair, and the outer
+    `not` again returns an Ω-pair. -/
+def or {ℓ : ULevel} (P Q : CTerm) : CTerm :=
+  not (ℓ := ℓ) (and (ℓ := ℓ) (not (ℓ := ℓ) P) (not (ℓ := ℓ) Q))
+
+/-- Universal quantifier over a base type: paired (Π-carrier code,
+    IsProp-of-Π code).
 
     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."
+    `forall_ T P` builds the Ω-pair whose carrier is the dependent
+    function space `Π x : T, .El (.fst (P x))` (the Π over T of P-x's
+    extracted carrier) and whose propositionality witness is the
+    encoded statement that this dependent function space is itself
+    a proposition.
 
-    ### CTerm shape
+    The dependent function space `Π x : T, B x` is a proposition
+    whenever `B x` is a proposition for every `x : T`: given
+    `f, g : Π x, B x`, propositionality of `B x` at each `x` gives
+    `f x = g x`, and funext lifts these pointwise equalities to
+    `f = g`.
 
-        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.
+    ### Encoding (ABI v5 universe codes)
 
-    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.
+        forall_ T P ≜ .pair
+          (.code (Π $x : T, .El (.fst (P $x))))
+          (.code (IsNType .negOne (Π $x : T, .El (.fst (P $x)))))
 
-    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")))
+    Both `T` and `P` are referenced inside the body — `T` as the
+    binder domain and `P` via `.app P (.var "$x")` inside the body.
+    The bound name `$x` is a real binder; references to `.var "$x"`
+    inside the body are scoped against the surrounding `.pi`. -/
+def forall_ {ℓ : ULevel} (T : CType ℓ) (P : CTerm) : CTerm :=
+  -- Dependent Π-carrier: pi over T whose body extracts P-x's
+  -- carrier code at each x via .El (.fst (P x)).  Uses
+  -- `CType.piSelf` to re-anchor at level `ℓ`.
+  let dpiCarrier : CType ℓ :=
+    CType.piSelf "$x" T (.El (ℓ := ℓ) (.fst (.app P (.var "$x"))))
+  .pair
+    (CTerm.code (ℓ := ℓ) dpiCarrier)
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne dpiCarrier))
 
-/-- Existential quantifier over a base type: paired ((‖Σ x : T,
-    P-of-x‖₋₁), propositionality-witness).
+/-- Existential quantifier over a base type: paired (truncated-Σ
+    carrier code, IsProp-of-truncated-Σ code).
 
     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).
+    the Ω-pair whose carrier is the propositional truncation
+    `‖Σ x : T, .El (.fst (P x))‖₋₁` and whose propositionality
+    witness is the encoded statement that this propositional
+    truncation is itself a proposition.
 
-    ### CTerm shape
+    Truncation is required: distinct witnesses `(x₁, w₁), (x₂, w₂)`
+    of the un-truncated Σ are not in general path-equal (e.g.,
+    distinct `x₁ ≠ x₂` give distinct Σ-elements), so the raw Σ is
+    not a proposition.  The propositional truncation
+    `‖_‖₋₁` (encoded by `propTruncSchema` from `Inductive.lean` and
+    exposed as `CType.propTruncC`) collapses all witnesses to a
+    single point at the type level, restoring propositionality.
 
-        exists_ T P  ≜  ctor propTruncSchema "inT" [⟨ℓ, T⟩]
-                            [pair (var "$witness") (fst (app P (var "$witness")))]
+    ### Encoding (ABI v5 universe codes)
 
-    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).
+        exists_ T P ≜ .pair
+          (.code (propTruncC (Σ $x : T, .El (.fst (P $x)))))
+          (.code (IsNType .negOne
+                    (propTruncC (Σ $x : T, .El (.fst (P $x))))))
 
-    The bound name `$witness` is bound by the outer `.lam` shown
-    below — making the inner `.var "$witness"` a real binder
-    reference. -/
+    Both `T` and `P` are referenced inside the body — `T` as the
+    Σ-binder domain and `P` via `.app P (.var "$x")` inside the
+    Σ-body.  The bound name `$x` is a real binder; references to
+    `.var "$x"` inside the Σ-body are scoped against the
+    surrounding `.sigma`. -/
 def exists_ {ℓ : ULevel} (T : CType ℓ) (P : CTerm) : CTerm :=
-  .lam "$witness"
-    (.ctor propTruncSchema "inT" [⟨ℓ, T⟩]
-      [.pair (.var "$witness") (.fst (.app P (.var "$witness")))])
+  -- Truncated Σ-carrier: ‖Σ $x : T, .El (.fst (P $x))‖₋₁.  Uses
+  -- `CType.sigmaSelf` to re-anchor the inner Σ at level `ℓ`,
+  -- then wraps in `CType.propTruncC` (which preserves level).
+  let sigmaCarrier : CType ℓ :=
+    CType.propTruncC
+      (CType.sigmaSelf "$x" T
+        (.El (ℓ := ℓ) (.fst (.app P (.var "$x")))))
+  .pair
+    (CTerm.code (ℓ := ℓ) sigmaCarrier)
+    (CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne sigmaCarrier))
 
 end Ω