diff --git a/native/cubical/include/cubical_transport.h b/native/cubical/include/cubical_transport.h
index 701bf86..0c5c29b 100644
--- a/native/cubical/include/cubical_transport.h
+++ b/native/cubical/include/cubical_transport.h
@@ -9,6 +9,43 @@
 //   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).
+//   6 — Modal cascade Phase 2 (cohesive triple ♭ ⊣ ♯ ⊣ ʃ).  Adds:
+//         CType.flat / .sharp / .shape  (tags 9 / 10 / 11)
+//         CTerm.{flat,sharp,shape}Intro (tags 17 / 18 / 19)
+//         CTerm.{flat,sharp,shape}Elim  (tags 20 / 21 / 22)
+//         CVal.v{Flat,Sharp,Shape}Intro (tags 12 / 13 / 14)
+//         CNeu.n{flat,sharp,shape}Elim  (tags 12 / 13 / 14)
+//       Layouts (Lean keeps implicit `{ℓ}` at runtime — same v4 rule):
+//         CType.flat  {ℓ} A            : 2 fields — [ℓ, A]
+//         CType.sharp {ℓ} A            : 2 fields — [ℓ, A]
+//         CType.shape {ℓ} A            : 2 fields — [ℓ, A]
+//         CTerm.flatIntro  a           : 1 field  — [a]   (no implicit ℓ)
+//         CTerm.sharpIntro a           : 1 field  — [a]
+//         CTerm.shapeIntro a           : 1 field  — [a]
+//         CTerm.flatElim   f m         : 2 fields — [f, m]
+//         CTerm.sharpElim  f m         : 2 fields — [f, m]
+//         CTerm.shapeElim  f m         : 2 fields — [f, m]
+//         CVal.vFlatIntro  v           : 1 field  — [v]   (CVal payload)
+//         CVal.vSharpIntro v           : 1 field  — [v]
+//         CVal.vShapeIntro v           : 1 field  — [v]
+//         CNeu.nflatElim   f n         : 2 fields — [f, n] (eliminator
+//                                                   value, stuck CNeu)
+//         CNeu.nsharpElim  f n         : 2 fields — [f, n]
+//         CNeu.nshapeElim  f n         : 2 fields — [f, n]
+//       Reductions (mirror Cubical/Eval.lean exactly):
+//         eval env (.flatIntro a)
+//             = .vFlatIntro (eval env a)         (similarly sharp/shape)
+//         eval env (.flatElim f m) =
+//             match eval env m with
+//             | .vFlatIntro a → vApp (eval env f) a            (β)
+//             | .vneu n       → .vneu (.nflatElim (eval env f) n)
+//             | _             → marker neutral (.nvar "<...>")
+//       Modal-type-driven transport / composition reductions are
+//       intentionally absent: a `transp i {flat A} φ t` falls through
+//       to the existing stuck-neutral path (transport.rs / composition.rs
+//       only have explicit arms for TY_PI; everything else stucks via
+//       ntransp / nhcomp / ncomp).  Modal cohesion-driven reductions
+//       (`flat`-transport, `shape`-shape law) land in Phase 3.
 //   5 — CType.El (decoder) and CTerm.code (encoder) constructors for
 //       universe-coding.  Adds CVal.vcode value form.  Layouts:
 //         CType.El {ℓ} P              : 2 fields — [ℓ, P]
@@ -57,6 +94,21 @@
 //             CType.El {ℓ} P                   → 2 slots: [ℓ, P]    (v5)
 //             CTerm.code {ℓ} A                 → 2 slots: [ℓ, A]    (v5)
 //             CVal.vcode {ℓ} A                 → 2 slots: [ℓ, A]    (v5)
+//             CType.flat  {ℓ} A                → 2 slots: [ℓ, A]    (v6)
+//             CType.sharp {ℓ} A                → 2 slots: [ℓ, A]    (v6)
+//             CType.shape {ℓ} A                → 2 slots: [ℓ, A]    (v6)
+//             CTerm.flatIntro  a               → 1 slot:  [a]       (v6)
+//             CTerm.sharpIntro a               → 1 slot:  [a]       (v6)
+//             CTerm.shapeIntro a               → 1 slot:  [a]       (v6)
+//             CTerm.flatElim   f m             → 2 slots: [f, m]    (v6)
+//             CTerm.sharpElim  f m             → 2 slots: [f, m]    (v6)
+//             CTerm.shapeElim  f m             → 2 slots: [f, m]    (v6)
+//             CVal.vFlatIntro  v               → 1 slot:  [v]       (v6)
+//             CVal.vSharpIntro v               → 1 slot:  [v]       (v6)
+//             CVal.vShapeIntro v               → 1 slot:  [v]       (v6)
+//             CNeu.nflatElim   f n             → 2 slots: [f, n]    (v6)
+//             CNeu.nsharpElim  f n             → 2 slots: [f, n]    (v6)
+//             CNeu.nshapeElim  f n             → 2 slots: [f, n]    (v6)
 //             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]
@@ -76,7 +128,7 @@
 #pragma once
 #include <lean/lean.h>
 
-#define CUBICAL_TRANSPORT_ABI_VERSION 5
+#define CUBICAL_TRANSPORT_ABI_VERSION 6
 
 #ifdef __cplusplus
 extern "C" {
diff --git a/native/cubical/src/dim_absent.rs b/native/cubical/src/dim_absent.rs
index 14265c9..cfb61d7 100644
--- a/native/cubical/src/dim_absent.rs
+++ b/native/cubical/src/dim_absent.rs
@@ -124,6 +124,21 @@ pub(crate) fn cterm_absent(i: LeanObj, t: LeanObj) -> bool {
         // ABI v5: universe-code encoder.  Same approximation as
         // transp/comp — A (the CType payload) is not recursed into.
         TERM_CODE => true,
+        // ABI v6: modal introductions — dim-absence preserved through
+        // the wrapper.  Layout: [a].  Mirrors Lean CTerm.dimAbsent arms
+        // for .flatIntro / .sharpIntro / .shapeIntro.
+        TERM_FLAT_INTRO | TERM_SHARP_INTRO | TERM_SHAPE_INTRO => {
+            let a = ctor_field(t, 0);
+            cterm_absent(i, a)
+        }
+        // ABI v6: modal eliminations — check both eliminator and
+        // scrutinee.  Layout: [f, m].  Mirrors Lean CTerm.dimAbsent
+        // arms for .flatElim / .sharpElim / .shapeElim.
+        TERM_FLAT_ELIM | TERM_SHARP_ELIM | TERM_SHAPE_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            cterm_absent(i, f) && cterm_absent(i, m)
+        }
         _ => true,
     }
 }
@@ -217,6 +232,13 @@ pub(crate) fn ctype_absent(i: LeanObj, a: LeanObj) -> bool {
             let p = ctor_field(a, 1);
             cterm_absent(i, p)
         }
+        // ABI v6: cohesive modalities — recurse into the wrapped CType.
+        // Layout: [ℓ, A].  Mirrors Lean CType.dimAbsent arms for
+        // .flat / .sharp / .shape.
+        TY_FLAT | TY_SHARP | TY_SHAPE => {
+            let inner = ctor_field(a, 1);
+            ctype_absent(i, inner)
+        }
         _ => true,
     }
 }
diff --git a/native/cubical/src/eval.rs b/native/cubical/src/eval.rs
index cd66c52..b97b2d5 100644
--- a/native/cubical/src/eval.rs
+++ b/native/cubical/src/eval.rs
@@ -238,6 +238,117 @@ pub fn eval(env: LeanObj, t: LeanObj) -> LeanObjMut {
             retain(l); retain(a);
             mk_vcode(l, a)
         }
+        TERM_FLAT_INTRO => {
+            // .flatIntro a — ABI v6: η_♭ intro.  Layout: [a] (1 field, no ℓ).
+            //   eval env (.flatIntro a) = .vFlatIntro (eval env a)
+            // (mirror Cubical/Eval.lean axiom eval_flatIntro).
+            let a = ctor_field(t, 0);
+            let va = eval(env, a);
+            mk_vflat_intro(va as LeanObj)
+        }
+        TERM_SHARP_INTRO => {
+            let a = ctor_field(t, 0);
+            let va = eval(env, a);
+            mk_vsharp_intro(va as LeanObj)
+        }
+        TERM_SHAPE_INTRO => {
+            let a = ctor_field(t, 0);
+            let va = eval(env, a);
+            mk_vshape_intro(va as LeanObj)
+        }
+        TERM_FLAT_ELIM => {
+            // .flatElim f m — ABI v6: ♭.rec.  Layout: [f, m] (2 fields).
+            //   eval env (.flatElim f m) =
+            //     match eval env m with
+            //     | .vFlatIntro a → vApp (eval env f) a    (β-rule)
+            //     | .vneu n       → .vneu (.nflatElim (eval env f) n)
+            //     | _             → marker neutral
+            // (mirror Cubical/Eval.lean axioms eval_flatElim_beta /
+            // eval_flatElim_stuck.)
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let vm = eval(env, m);
+            let vm_ro = vm as LeanObj;
+            match ctor_tag(vm_ro) {
+                VAL_VFLAT_INTRO => {
+                    // β-reduce: extract the wrapped value, drop the
+                    // outer .vFlatIntro, and apply f to it.
+                    let inner = ctor_field(vm_ro, 0);
+                    retain(inner);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    vapp(vf, inner as LeanObjMut)
+                }
+                VAL_VNEU => {
+                    // Stuck: extract the inner CNeu, build .nflatElim
+                    // with the evaluated eliminator function.
+                    let inner_neu = ctor_field(vm_ro, 0);
+                    retain(inner_neu);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    let nelim = mk_nflat_elim(vf as LeanObj, inner_neu);
+                    mk_vneu(nelim as LeanObj)
+                }
+                _ => {
+                    release(vm_ro);
+                    stuck_marker(b"<flatElim: scrutinee is not flat-canonical>\0")
+                }
+            }
+        }
+        TERM_SHARP_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let vm = eval(env, m);
+            let vm_ro = vm as LeanObj;
+            match ctor_tag(vm_ro) {
+                VAL_VSHARP_INTRO => {
+                    let inner = ctor_field(vm_ro, 0);
+                    retain(inner);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    vapp(vf, inner as LeanObjMut)
+                }
+                VAL_VNEU => {
+                    let inner_neu = ctor_field(vm_ro, 0);
+                    retain(inner_neu);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    let nelim = mk_nsharp_elim(vf as LeanObj, inner_neu);
+                    mk_vneu(nelim as LeanObj)
+                }
+                _ => {
+                    release(vm_ro);
+                    stuck_marker(b"<sharpElim: scrutinee is not sharp-canonical>\0")
+                }
+            }
+        }
+        TERM_SHAPE_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let vm = eval(env, m);
+            let vm_ro = vm as LeanObj;
+            match ctor_tag(vm_ro) {
+                VAL_VSHAPE_INTRO => {
+                    let inner = ctor_field(vm_ro, 0);
+                    retain(inner);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    vapp(vf, inner as LeanObjMut)
+                }
+                VAL_VNEU => {
+                    let inner_neu = ctor_field(vm_ro, 0);
+                    retain(inner_neu);
+                    release(vm_ro);
+                    let vf = eval(env, f);
+                    let nelim = mk_nshape_elim(vf as LeanObj, inner_neu);
+                    mk_vneu(nelim as LeanObj)
+                }
+                _ => {
+                    release(vm_ro);
+                    stuck_marker(b"<shapeElim: scrutinee is not shape-canonical>\0")
+                }
+            }
+        }
         TERM_INDELIM => {
             // .indElim S params motive branches target — β-reduce on a
             // canonical vctor target; otherwise build .nIndElim stuck.
@@ -402,8 +513,12 @@ pub fn vapp(f: LeanObjMut, a: LeanObjMut) -> LeanObjMut {
             release(f_ro);
             result
         }
-        VAL_VPLAM | VAL_VTUBEAPP | VAL_VPATHTRANSP | VAL_VPAIR | VAL_VCODE => {
+        VAL_VPLAM | VAL_VTUBEAPP | VAL_VPATHTRANSP | VAL_VPAIR | VAL_VCODE
+        | VAL_VFLAT_INTRO | VAL_VSHARP_INTRO | VAL_VSHAPE_INTRO => {
             // Ill-typed application; marker neutral per FFI_DESIGN §6.
+            // ABI v6: modal intros are not functions either — they
+            // mirror the Lean `eval`'s explicit arm for vFlat/Sharp/
+            // ShapeIntro applied as a function.
             release(f_ro);
             release(a as LeanObj);
             stuck_marker(b"<vApp: non-function value applied>\0")
diff --git a/native/cubical/src/readback.rs b/native/cubical/src/readback.rs
index d132696..064f419 100644
--- a/native/cubical/src/readback.rs
+++ b/native/cubical/src/readback.rs
@@ -583,6 +583,30 @@ pub fn readback(v: LeanObj) -> LeanObjMut {
             retain(l); retain(a);
             mk_term_code(l, a)
         }
+        // ABI v6: modal-introduction values.  Layout: [v] (1 field).
+        // Mirrors Cubical/Readback.lean axioms readback_vFlatIntro etc.
+        VAL_VFLAT_INTRO => {
+            // readback (.vFlatIntro a) = .flatIntro (readback a)
+            let inner = ctor_field(v, 0);
+            let inner_term = readback(inner);
+            let ctor = alloc_ctor(TERM_FLAT_INTRO, 1);
+            ctor_set_field(ctor, 0, inner_term as LeanObj);
+            ctor
+        }
+        VAL_VSHARP_INTRO => {
+            let inner = ctor_field(v, 0);
+            let inner_term = readback(inner);
+            let ctor = alloc_ctor(TERM_SHARP_INTRO, 1);
+            ctor_set_field(ctor, 0, inner_term as LeanObj);
+            ctor
+        }
+        VAL_VSHAPE_INTRO => {
+            let inner = ctor_field(v, 0);
+            let inner_term = readback(inner);
+            let ctor = alloc_ctor(TERM_SHAPE_INTRO, 1);
+            ctor_set_field(ctor, 0, inner_term as LeanObj);
+            ctor
+        }
         _ => {
             // Malformed — return a marker var.
             let msg = unsafe {
@@ -712,6 +736,41 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut {
             mk_term_indelim(schema, params, motive_term as LeanObj,
                             branches_term as LeanObj, target_term as LeanObj)
         }
+        // ABI v6: modal-elimination stuck neutrals.  Layout: [f, n] —
+        // field 0 is the evaluated eliminator function (a CVal),
+        // field 1 is the stuck scrutinee (a CNeu).  Mirrors
+        // Cubical/Readback.lean readbackNeu_nflatElim etc.
+        NEU_NFLAT_ELIM => {
+            // readbackNeu (.nflatElim f n) = .flatElim (readback f) (readbackNeu n)
+            let f = ctor_field(n, 0);
+            let inner_neu = ctor_field(n, 1);
+            let f_term = readback(f);
+            let inner_term = readback_neu(inner_neu);
+            let ctor = alloc_ctor(TERM_FLAT_ELIM, 2);
+            ctor_set_field(ctor, 0, f_term as LeanObj);
+            ctor_set_field(ctor, 1, inner_term as LeanObj);
+            ctor
+        }
+        NEU_NSHARP_ELIM => {
+            let f = ctor_field(n, 0);
+            let inner_neu = ctor_field(n, 1);
+            let f_term = readback(f);
+            let inner_term = readback_neu(inner_neu);
+            let ctor = alloc_ctor(TERM_SHARP_ELIM, 2);
+            ctor_set_field(ctor, 0, f_term as LeanObj);
+            ctor_set_field(ctor, 1, inner_term as LeanObj);
+            ctor
+        }
+        NEU_NSHAPE_ELIM => {
+            let f = ctor_field(n, 0);
+            let inner_neu = ctor_field(n, 1);
+            let f_term = readback(f);
+            let inner_term = readback_neu(inner_neu);
+            let ctor = alloc_ctor(TERM_SHAPE_ELIM, 2);
+            ctor_set_field(ctor, 0, f_term as LeanObj);
+            ctor_set_field(ctor, 1, inner_term as LeanObj);
+            ctor
+        }
         _ => {
             let msg = unsafe {
                 lean_mk_string(b"<readbackNeu: unknown CNeu>\0".as_ptr() as *const core::ffi::c_char)
diff --git a/native/cubical/src/subst.rs b/native/cubical/src/subst.rs
index 2f1a638..20ab8c1 100644
--- a/native/cubical/src/subst.rs
+++ b/native/cubical/src/subst.rs
@@ -552,6 +552,61 @@ pub(crate) fn cterm_subst_dim(i: LeanObj, r: LeanObj, t: LeanObj) -> LeanObjMut
             retain(t);
             t as LeanObjMut
         }
+        // ABI v6: modal introductions — recurse into the wrapped CTerm.
+        // Layout: [a] (1 field, no implicit ℓ).
+        TERM_FLAT_INTRO => {
+            let a = ctor_field(t, 0);
+            let na = cterm_subst_dim(i, r, a);
+            let ctor = alloc_ctor(TERM_FLAT_INTRO, 1);
+            ctor_set_field(ctor, 0, na as LeanObj);
+            ctor
+        }
+        TERM_SHARP_INTRO => {
+            let a = ctor_field(t, 0);
+            let na = cterm_subst_dim(i, r, a);
+            let ctor = alloc_ctor(TERM_SHARP_INTRO, 1);
+            ctor_set_field(ctor, 0, na as LeanObj);
+            ctor
+        }
+        TERM_SHAPE_INTRO => {
+            let a = ctor_field(t, 0);
+            let na = cterm_subst_dim(i, r, a);
+            let ctor = alloc_ctor(TERM_SHAPE_INTRO, 1);
+            ctor_set_field(ctor, 0, na as LeanObj);
+            ctor
+        }
+        // ABI v6: modal eliminations — recurse into both subterms.
+        // Layout: [f, m] (2 fields).
+        TERM_FLAT_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let nf = cterm_subst_dim(i, r, f);
+            let nm = cterm_subst_dim(i, r, m);
+            let ctor = alloc_ctor(TERM_FLAT_ELIM, 2);
+            ctor_set_field(ctor, 0, nf as LeanObj);
+            ctor_set_field(ctor, 1, nm as LeanObj);
+            ctor
+        }
+        TERM_SHARP_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let nf = cterm_subst_dim(i, r, f);
+            let nm = cterm_subst_dim(i, r, m);
+            let ctor = alloc_ctor(TERM_SHARP_ELIM, 2);
+            ctor_set_field(ctor, 0, nf as LeanObj);
+            ctor_set_field(ctor, 1, nm as LeanObj);
+            ctor
+        }
+        TERM_SHAPE_ELIM => {
+            let f = ctor_field(t, 0);
+            let m = ctor_field(t, 1);
+            let nf = cterm_subst_dim(i, r, f);
+            let nm = cterm_subst_dim(i, r, m);
+            let ctor = alloc_ctor(TERM_SHAPE_ELIM, 2);
+            ctor_set_field(ctor, 0, nf as LeanObj);
+            ctor_set_field(ctor, 1, nm as LeanObj);
+            ctor
+        }
         _ => {
             // Unknown tag — preserve identity by retaining + boxing as
             // raw object (no malformed-CTerm corruption).
@@ -731,6 +786,33 @@ fn mk_ty_el(l: LeanObj, p: LeanObj) -> LeanObjMut {
     ctor
 }
 
+/// `.flat {ℓ} A` — ABI v6 cohesive-modality (♭).  Layout: [ℓ, A].
+#[inline]
+fn mk_ty_flat(l: LeanObj, a: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TY_FLAT, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, a);
+    ctor
+}
+
+/// `.sharp {ℓ} A` — ABI v6 cohesive-modality (♯).  Layout: [ℓ, A].
+#[inline]
+fn mk_ty_sharp(l: LeanObj, a: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TY_SHARP, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, a);
+    ctor
+}
+
+/// `.shape {ℓ} A` — ABI v6 cohesive-modality (ʃ).  Layout: [ℓ, A].
+#[inline]
+fn mk_ty_shape(l: LeanObj, a: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TY_SHAPE, 2);
+    ctor_set_field(ctor, 0, l);
+    ctor_set_field(ctor, 1, a);
+    ctor
+}
+
 /// `.glue {ℓ} φ T f fInv sec ret coh A` — 9 fields.
 #[inline]
 fn mk_ty_glue(
@@ -868,6 +950,30 @@ pub(crate) fn ctype_subst_dim_bool(i: LeanObj, b: bool, a: LeanObj) -> LeanObjMu
             let new_p = cterm_subst_dim_bool(i, b, p);
             mk_ty_el(l, new_p as LeanObj)
         }
+        // ABI v6: cohesive modalities — recurse into the wrapped CType.
+        // Layout: [ℓ, A].  Mirrors Lean's CType.substDim arms for
+        // .flat / .sharp / .shape.
+        TY_FLAT => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_bool(i, b, inner);
+            mk_ty_flat(l, new_inner as LeanObj)
+        }
+        TY_SHARP => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_bool(i, b, inner);
+            mk_ty_sharp(l, new_inner as LeanObj)
+        }
+        TY_SHAPE => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_bool(i, b, inner);
+            mk_ty_shape(l, new_inner as LeanObj)
+        }
         _ => {
             // Synthetic fallback at level zero.
             mk_ty_univ(lean_box_mut(0) as LeanObj)
@@ -1008,6 +1114,29 @@ pub(crate) fn ctype_subst_dim_expr(i: LeanObj, r: LeanObj, a: LeanObj) -> LeanOb
             let new_p = cterm_subst_dim(i, r, p);
             mk_ty_el(l, new_p as LeanObj)
         }
+        // ABI v6: cohesive modalities — recurse into the wrapped CType.
+        // Layout: [ℓ, A].  Mirrors Lean's CType.substDimExpr arms.
+        TY_FLAT => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_expr(i, r, inner);
+            mk_ty_flat(l, new_inner as LeanObj)
+        }
+        TY_SHARP => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_expr(i, r, inner);
+            mk_ty_sharp(l, new_inner as LeanObj)
+        }
+        TY_SHAPE => {
+            let l = ctor_field(a, 0);
+            let inner = ctor_field(a, 1);
+            retain(l);
+            let new_inner = ctype_subst_dim_expr(i, r, inner);
+            mk_ty_shape(l, new_inner 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 404af23..a6ce43b 100644
--- a/native/cubical/src/tags.rs
+++ b/native/cubical/src/tags.rs
@@ -46,6 +46,9 @@ 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`
+pub const TY_FLAT:     u32 = 9;  // ABI v6: cohesive modality `♭ A` (flat)
+pub const TY_SHARP:    u32 = 10; // ABI v6: cohesive modality `♯ A` (sharp)
+pub const TY_SHAPE:    u32 = 11; // ABI v6: cohesive modality `ʃ A` (shape)
 
 // ── CTerm (Cubical/Syntax.lean) ────────────────────────────────────────────
 
@@ -66,6 +69,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`
+pub const TERM_FLAT_INTRO:   u32 = 17;  // ABI v6: η_♭ — flatIntro a
+pub const TERM_SHARP_INTRO:  u32 = 18;  // ABI v6: η_♯ — sharpIntro a
+pub const TERM_SHAPE_INTRO:  u32 = 19;  // ABI v6: η_ʃ — shapeIntro a
+pub const TERM_FLAT_ELIM:    u32 = 20;  // ABI v6: ♭.rec — flatElim f m
+pub const TERM_SHARP_ELIM:   u32 = 21;  // ABI v6: ♯.rec — sharpElim f m
+pub const TERM_SHAPE_ELIM:   u32 = 22;  // ABI v6: ʃ.rec — shapeElim f m
 
 // ── CEnv (Cubical/Value.lean) ──────────────────────────────────────────────
 
@@ -86,6 +95,9 @@ 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`
+pub const VAL_VFLAT_INTRO:  u32 = 12;  // ABI v6: vFlatIntro  v — η_♭ value
+pub const VAL_VSHARP_INTRO: u32 = 13;  // ABI v6: vSharpIntro v — η_♯ value
+pub const VAL_VSHAPE_INTRO: u32 = 14;  // ABI v6: vShapeIntro v — η_ʃ value
 
 // ── CNeu (Cubical/Value.lean) ──────────────────────────────────────────────
 
@@ -101,3 +113,6 @@ pub const NEU_NUNGLUE:  u32 = 8;
 pub const NEU_NFST:     u32 = 9;
 pub const NEU_NSND:     u32 = 10;
 pub const NEU_NINDELIM: u32 = 11;  // REL1: stuck inductive eliminator
+pub const NEU_NFLAT_ELIM:  u32 = 12;  // ABI v6: stuck nflatElim  f n
+pub const NEU_NSHARP_ELIM: u32 = 13;  // ABI v6: stuck nsharpElim f n
+pub const NEU_NSHAPE_ELIM: u32 = 14;  // ABI v6: stuck nshapeElim f n
diff --git a/native/cubical/src/value.rs b/native/cubical/src/value.rs
index ca5f6cc..9831a3b 100644
--- a/native/cubical/src/value.rs
+++ b/native/cubical/src/value.rs
@@ -322,6 +322,68 @@ pub(crate) fn mk_term_code(l: LeanObj, a: LeanObj) -> LeanObjMut {
     ctor
 }
 
+// ── ABI v6: cohesive modality value/neutral builders ───────────────────────
+//
+// Three intro values (vFlatIntro / vSharpIntro / vShapeIntro) carry one
+// CVal payload.  Three stuck-elim neutrals (nflatElim / nsharpElim /
+// nshapeElim) carry the evaluated eliminator function (CVal) and the
+// stuck scrutinee (CNeu).  No implicit ULevel — modal intros and
+// elims are CTerm/CVal-typed, not CType-typed (the modal's ULevel
+// lives on the surrounding CType.flat/.sharp/.shape, not here).
+
+/// `.vFlatIntro v` — η_♭ value (ABI v6).  Layout: `[v]` (1 field).
+#[inline]
+pub(crate) fn mk_vflat_intro(v: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VFLAT_INTRO, 1);
+    ctor_set_field(ctor, 0, v);
+    ctor
+}
+
+/// `.vSharpIntro v` — η_♯ value (ABI v6).  Layout: `[v]` (1 field).
+#[inline]
+pub(crate) fn mk_vsharp_intro(v: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VSHARP_INTRO, 1);
+    ctor_set_field(ctor, 0, v);
+    ctor
+}
+
+/// `.vShapeIntro v` — η_ʃ value (ABI v6).  Layout: `[v]` (1 field).
+#[inline]
+pub(crate) fn mk_vshape_intro(v: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VSHAPE_INTRO, 1);
+    ctor_set_field(ctor, 0, v);
+    ctor
+}
+
+/// `.nflatElim f n` — stuck flat-eliminator neutral (ABI v6).
+/// Layout: `[f, n]` (2 fields): the evaluated eliminator function and
+/// the stuck scrutinee.
+#[inline]
+pub(crate) fn mk_nflat_elim(f: LeanObj, n: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(NEU_NFLAT_ELIM, 2);
+    ctor_set_field(ctor, 0, f);
+    ctor_set_field(ctor, 1, n);
+    ctor
+}
+
+/// `.nsharpElim f n` — stuck sharp-eliminator neutral (ABI v6).
+#[inline]
+pub(crate) fn mk_nsharp_elim(f: LeanObj, n: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(NEU_NSHARP_ELIM, 2);
+    ctor_set_field(ctor, 0, f);
+    ctor_set_field(ctor, 1, n);
+    ctor
+}
+
+/// `.nshapeElim f n` — stuck shape-eliminator neutral (ABI v6).
+#[inline]
+pub(crate) fn mk_nshape_elim(f: LeanObj, n: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(NEU_NSHAPE_ELIM, 2);
+    ctor_set_field(ctor, 0, f);
+    ctor_set_field(ctor, 1, n);
+    ctor
+}
+
 /// `.nIndElim S params motive branches target` — stuck eliminator
 /// neutral.  Five fields per the Lean definition.  No implicit ULevel.
 #[inline]