diff --git a/CubicalTransport/DecEq.lean b/CubicalTransport/DecEq.lean
index 15037c6..8fbf8a8 100644
--- a/CubicalTransport/DecEq.lean
+++ b/CubicalTransport/DecEq.lean
@@ -61,6 +61,12 @@ partial def beqCTypeAny : (Σ ℓ : ULevel, CType ℓ) → (Σ ℓ : ULevel, CTy
       beqCTypeAny ⟨_, A⟩ ⟨_, A'⟩
   | ⟨_, .El P⟩, ⟨_, .El Q⟩ =>
       beqCTerm P Q
+  | ⟨_, .flat A⟩, ⟨_, .flat B⟩ =>
+      beqCTypeAny ⟨_, A⟩ ⟨_, B⟩
+  | ⟨_, .sharp A⟩, ⟨_, .sharp B⟩ =>
+      beqCTypeAny ⟨_, A⟩ ⟨_, B⟩
+  | ⟨_, .shape A⟩, ⟨_, .shape B⟩ =>
+      beqCTypeAny ⟨_, A⟩ ⟨_, B⟩
   | _, _ => false
 
 partial def beqCTerm : CTerm → CTerm → Bool
@@ -94,6 +100,14 @@ partial def beqCTerm : CTerm → CTerm → Bool
       -- A and B may live at different universe levels.  Route through
       -- the level-erased Σ-pair beq to compare them honestly.
       beqCTypeAny ⟨_, A⟩ ⟨_, B⟩
+  -- Modal introductions: structural equality on the wrapped term.
+  | .flatIntro a, .flatIntro b => beqCTerm a b
+  | .sharpIntro a, .sharpIntro b => beqCTerm a b
+  | .shapeIntro a, .shapeIntro b => beqCTerm a b
+  -- Modal eliminations: structural equality on (eliminator, scrutinee).
+  | .flatElim f m, .flatElim f' m' => beqCTerm f f' && beqCTerm m m'
+  | .sharpElim f m, .sharpElim f' m' => beqCTerm f f' && beqCTerm m m'
+  | .shapeElim f m, .shapeElim f' m' => beqCTerm f f' && beqCTerm m m'
   | _, _ => false
 
 partial def beqCTypeArg : CTypeArg → CTypeArg → Bool
diff --git a/CubicalTransport/DimLine.lean b/CubicalTransport/DimLine.lean
index 4cf400a..174ee9d 100644
--- a/CubicalTransport/DimLine.lean
+++ b/CubicalTransport/DimLine.lean
@@ -93,6 +93,14 @@ mutual
     -- substDim approximation in Syntax.lean — the CType payload is
     -- conservatively assumed to be dim-stable).
     | .code _         => true
+    -- Modal introductions: dim-absence is preserved through the wrapper.
+    | .flatIntro a    => a.dimAbsent i
+    | .sharpIntro a   => a.dimAbsent i
+    | .shapeIntro a   => a.dimAbsent i
+    -- Modal eliminations: check both the eliminator and the scrutinee.
+    | .flatElim f m   => f.dimAbsent i && m.dimAbsent i
+    | .sharpElim f m  => f.dimAbsent i && m.dimAbsent i
+    | .shapeElim f m  => f.dimAbsent i && m.dimAbsent i
 
   /-- Helper: check that `i` is absent from every clause in a system. -/
   def CTerm.dimAbsent.clauses (i : DimVar) :
@@ -129,6 +137,10 @@ mutual
     | .interval          => true   -- REL2: 𝕀 carries no dim binders
     | .lift A            => A.dimAbsent i
     | .El P              => P.dimAbsent i
+    -- Modal type formers: dim-absence reduces to the inner type's.
+    | .flat A            => A.dimAbsent i
+    | .sharp A           => A.dimAbsent i
+    | .shape A           => A.dimAbsent i
 
   /-- Helper: check `i` absent from every CType in a level-heterogeneous
       parameter list. -/
@@ -260,6 +272,33 @@ mutual
             CTerm.substDim.branches_of_absent i r branches hbr,
             CTerm.substDim_absent_aux i r target htg]
     | .code _, _ => rfl
+    | .flatIntro a, h => by
+        simp only [CTerm.dimAbsent] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r a h]
+    | .sharpIntro a, h => by
+        simp only [CTerm.dimAbsent] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r a h]
+    | .shapeIntro a, h => by
+        simp only [CTerm.dimAbsent] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r a h]
+    | .flatElim f m, h => by
+        simp only [CTerm.dimAbsent, Bool.and_eq_true] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r f h.1,
+            CTerm.substDim_absent_aux i r m h.2]
+    | .sharpElim f m, h => by
+        simp only [CTerm.dimAbsent, Bool.and_eq_true] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r f h.1,
+            CTerm.substDim_absent_aux i r m h.2]
+    | .shapeElim f m, h => by
+        simp only [CTerm.dimAbsent, Bool.and_eq_true] at h
+        simp only [CTerm.substDim]
+        rw [CTerm.substDim_absent_aux i r f h.1,
+            CTerm.substDim_absent_aux i r m h.2]
 
   /-- Helper: `substDim.clauses` is identity on clause lists whose every
       `(face, body)` pair has `i` absent. -/
@@ -375,6 +414,21 @@ mutual
         show CType.El (CTerm.substDimBool i b P) = CType.El P
         congr 1
         exact CTerm.substDimBool_of_absent i b P h
+    | .flat A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.flat (CType.substDim i b A) = CType.flat A
+        congr 1
+        exact CType.substDim_absent_aux i b A h
+    | .sharp A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.sharp (CType.substDim i b A) = CType.sharp A
+        congr 1
+        exact CType.substDim_absent_aux i b A h
+    | .shape A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.shape (CType.substDim i b A) = CType.shape A
+        congr 1
+        exact CType.substDim_absent_aux i b A h
 
   /-- Helper: `CType.substDim.params i b` is identity on level-
       heterogeneous parameter lists with `i` absent from every entry. -/
@@ -454,6 +508,21 @@ mutual
         show CType.El (CTerm.substDim i r P) = CType.El P
         congr 1
         exact CTerm.substDim_of_absent i r P h
+    | .flat A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.flat (A.substDimExpr i r) = CType.flat A
+        congr 1
+        exact CType.substDimExpr_absent_aux i r A h
+    | .sharp A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.sharp (A.substDimExpr i r) = CType.sharp A
+        congr 1
+        exact CType.substDimExpr_absent_aux i r A h
+    | .shape A, h => by
+        simp only [CType.dimAbsent] at h
+        show CType.shape (A.substDimExpr i r) = CType.shape A
+        congr 1
+        exact CType.substDimExpr_absent_aux i r A h
 
   /-- Helper: `CType.substDimExpr.params i r` is identity on level-
       heterogeneous parameter lists with `i` absent from every entry. -/
@@ -605,6 +674,27 @@ mutual
           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]
+    | .flatIntro a => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr a]
+    | .sharpIntro a => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr a]
+    | .shapeIntro a => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr a]
+    | .flatElim f m => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr f,
+          CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self]
+    | .sharpElim f m => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr f,
+          CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self]
+    | .shapeElim f m => by
+        simp only [CTerm.substDim, CTerm.dimAbsent,
+          CTerm.dimAbsent_after_substDim_aux i r hr f,
+          CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self]
 
   /-- Helper: `i` is absent from every clause in the result of substituting
       `i := r` in a clause list (provided `r` doesn't mention `i`). -/
@@ -690,6 +780,15 @@ mutual
     | .El P => by
         simp only [CType.substDim, CType.dimAbsent]
         exact CTerm.dimAbsent_after_substDimBool i b P
+    | .flat A => by
+        simp only [CType.substDim, CType.dimAbsent,
+          CType.dimAbsent_after_substDim_aux i b A]
+    | .sharp A => by
+        simp only [CType.substDim, CType.dimAbsent,
+          CType.dimAbsent_after_substDim_aux i b A]
+    | .shape A => by
+        simp only [CType.substDim, CType.dimAbsent,
+          CType.dimAbsent_after_substDim_aux i b A]
 
   /-- Helper: `i` absent from every CType in `substDim.params i b ps`. -/
   private def CType.dimAbsent.params_after_substDim (i : DimVar) (b : Bool) :
@@ -851,6 +950,33 @@ mutual
         · 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
+    | .flatIntro a => by
+        simp only [CTerm.substDim]
+        exact congrArg CTerm.flatIntro
+          (CTerm.substDim_comm_aux i j r s hij hrj hsi a)
+    | .sharpIntro a => by
+        simp only [CTerm.substDim]
+        exact congrArg CTerm.sharpIntro
+          (CTerm.substDim_comm_aux i j r s hij hrj hsi a)
+    | .shapeIntro a => by
+        simp only [CTerm.substDim]
+        exact congrArg CTerm.shapeIntro
+          (CTerm.substDim_comm_aux i j r s hij hrj hsi a)
+    | .flatElim f m => by
+        simp only [CTerm.substDim]
+        congr 1
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi m
+    | .sharpElim f m => by
+        simp only [CTerm.substDim]
+        congr 1
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi m
+    | .shapeElim f m => by
+        simp only [CTerm.substDim]
+        congr 1
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f
+        · exact CTerm.substDim_comm_aux i j r s hij hrj hsi m
 
   /-- Helper: `substDim.clauses` commutes on disjoint dim variables. -/
   private def CTerm.substDim.clauses_comm_aux
@@ -950,6 +1076,18 @@ mutual
         simp only [CType.substDim]
         congr 1
         exact CTerm.substDimBool_comm i j b c hij P
+    | .flat A => by
+        simp only [CType.substDim]
+        congr 1
+        exact CType.substDim_comm_aux i j b c hij A
+    | .sharp A => by
+        simp only [CType.substDim]
+        congr 1
+        exact CType.substDim_comm_aux i j b c hij A
+    | .shape A => by
+        simp only [CType.substDim]
+        congr 1
+        exact CType.substDim_comm_aux i j b c hij A
 
   /-- 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 13dcdda..1306539 100644
--- a/CubicalTransport/Eval.lean
+++ b/CubicalTransport/Eval.lean
@@ -161,6 +161,28 @@ mutual
                     (branches.map (fun (nm, b) => (nm, eval env b))) n)
         | _ =>
             .vneu (.nvar "<indElim: target is not canonical>")
+    -- Modal introductions: structural lift to the corresponding value form.
+    | .flatIntro a   => .vFlatIntro  (eval env a)
+    | .sharpIntro a  => .vSharpIntro (eval env a)
+    | .shapeIntro a  => .vShapeIntro (eval env a)
+    -- Modal eliminations: β-reduce on the corresponding intro value form;
+    -- otherwise produce a stuck neutral that preserves the evaluated
+    -- eliminator function and the (necessarily-stuck) scrutinee neutral.
+    | .flatElim f m =>
+        match eval env m with
+        | .vFlatIntro a => vApp (eval env f) a
+        | .vneu n       => .vneu (.nflatElim (eval env f) n)
+        | _             => .vneu (.nvar "<flatElim: scrutinee is not flat-canonical>")
+    | .sharpElim f m =>
+        match eval env m with
+        | .vSharpIntro a => vApp (eval env f) a
+        | .vneu n        => .vneu (.nsharpElim (eval env f) n)
+        | _              => .vneu (.nvar "<sharpElim: scrutinee is not sharp-canonical>")
+    | .shapeElim f m =>
+        match eval env m with
+        | .vShapeIntro a => vApp (eval env f) a
+        | .vneu n        => .vneu (.nshapeElim (eval env f) n)
+        | _              => .vneu (.nvar "<shapeElim: scrutinee is not shape-canonical>")
 
   /-- First projection at the value level.  β-reduces `vpair`; pushes a
       stuck neutral into `nfst`.  Projecting any other value shape is a
@@ -221,6 +243,9 @@ mutual
     | .vctor _ _ _ _,               _   => .vneu (.nvar "<vApp: vctor applied as function>")
     | .vdimExpr _,                  _   => .vneu (.nvar "<vApp: vdimExpr applied as function>")
     | .vcode _,                     _   => .vneu (.nvar "<vApp: vcode applied as function>")
+    | .vFlatIntro _,                _   => .vneu (.nvar "<vApp: vFlatIntro applied as function>")
+    | .vSharpIntro _,               _   => .vneu (.nvar "<vApp: vSharpIntro applied as function>")
+    | .vShapeIntro _,               _   => .vneu (.nvar "<vApp: vShapeIntro 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
@@ -254,6 +279,9 @@ mutual
     | .vctor _ _ _ _,           _ => .vneu (.nvar "<vPApp: vctor applied as path>")
     | .vdimExpr _,              _ => .vneu (.nvar "<vPApp: vdimExpr applied as path>")
     | .vcode _,                 _ => .vneu (.nvar "<vPApp: vcode applied as path>")
+    | .vFlatIntro _,            _ => .vneu (.nvar "<vPApp: vFlatIntro applied as path>")
+    | .vSharpIntro _,           _ => .vneu (.nvar "<vPApp: vSharpIntro applied as path>")
+    | .vShapeIntro _,           _ => .vneu (.nvar "<vPApp: vShapeIntro applied as path>")
 
   /-- Homogeneous composition at the value level.  The type `A` is
       *homogeneous* (doesn't vary along `i`); the tube and base are
@@ -867,3 +895,59 @@ preserving the underlying CType.  Mirrors `eval_dimExpr` (a similar
     to the corresponding `vcode` value form, preserving `A`. -/
 axiom eval_code {ℓ : ULevel} (env : CEnv) (A : CType ℓ) :
     eval env (.code A) = .vcode A
+
+/-!
+### `eval` on modal introductions / eliminations
+
+For each modality M ∈ {flat, sharp, shape}:
+  · `M-Intro a` evaluates to `vM-Intro (eval env a)` (lift through the
+    constructor).
+  · `M-Elim f m` β-reduces when the scrutinee evaluates to a `vM-Intro`,
+    via `vApp` with the eliminator function; on a stuck neutral it
+    produces a `nM-Elim` neutral; on any other shape, a marker neutral.
+
+The arms below mirror the partial-def cases verbatim.  Engine-layer
+axioms; modal-cohesion semantics (Crisp variables, `♭ ⊣ ♯ ⊣ ʃ`
+adjunction laws) are Phase 3 and live in a separate `Modal.lean`.
+-/
+
+-- Modal introductions: structural lift to the corresponding value form.
+
+axiom eval_flatIntro (env : CEnv) (a : CTerm) :
+    eval env (.flatIntro a) = .vFlatIntro (eval env a)
+
+axiom eval_sharpIntro (env : CEnv) (a : CTerm) :
+    eval env (.sharpIntro a) = .vSharpIntro (eval env a)
+
+axiom eval_shapeIntro (env : CEnv) (a : CTerm) :
+    eval env (.shapeIntro a) = .vShapeIntro (eval env a)
+
+-- Modal eliminations: β on the corresponding intro; stuck on neutrals.
+
+/-- β-rule: `flatElim f (flatIntro a)` reduces to `app f a` at the eval
+    level.  The scrutinee evaluates to `vFlatIntro (eval env a)`; the
+    elim arm of `eval` then invokes `vApp` on the eliminator value. -/
+axiom eval_flatElim_beta (env : CEnv) (f a : CTerm) :
+    eval env (.flatElim f (.flatIntro a)) = vApp (eval env f) (eval env a)
+
+axiom eval_sharpElim_beta (env : CEnv) (f a : CTerm) :
+    eval env (.sharpElim f (.sharpIntro a)) = vApp (eval env f) (eval env a)
+
+axiom eval_shapeElim_beta (env : CEnv) (f a : CTerm) :
+    eval env (.shapeElim f (.shapeIntro a)) = vApp (eval env f) (eval env a)
+
+/-- Stuck case: `flatElim` whose scrutinee evaluates to a CNeu produces
+    a `nflatElim` neutral preserving the evaluated function and
+    scrutinee.  The scrutinee must be `.vneu n` after eval; this is
+    encoded by the explicit hypothesis `eval env m = .vneu n`. -/
+axiom eval_flatElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu)
+    (h : eval env m = .vneu n) :
+    eval env (.flatElim f m) = .vneu (.nflatElim (eval env f) n)
+
+axiom eval_sharpElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu)
+    (h : eval env m = .vneu n) :
+    eval env (.sharpElim f m) = .vneu (.nsharpElim (eval env f) n)
+
+axiom eval_shapeElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu)
+    (h : eval env m = .vneu n) :
+    eval env (.shapeElim f m) = .vneu (.nshapeElim (eval env f) n)
diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean
index 4f45077..561491e 100644
--- a/CubicalTransport/FFITest.lean
+++ b/CubicalTransport/FFITest.lean
@@ -46,6 +46,9 @@ def cvalSummary : CVal → String
   | .vneu (.nfst _)             => "vneu nfst"
   | .vneu (.nsnd _)             => "vneu nsnd"
   | .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim"
+  | .vneu (.nflatElim _ _)      => "vneu nflatElim"
+  | .vneu (.nsharpElim _ _)     => "vneu nsharpElim"
+  | .vneu (.nshapeElim _ _)     => "vneu nshapeElim"
   | .vlam _ x _                 => s!"vlam {x} ..."
   | .vplam _ i _                => s!"vplam {i.name} ..."
   | .vpair _ _                  => "vpair ..."
@@ -57,6 +60,9 @@ def cvalSummary : CVal → String
   | .vctor _ c _ _              => s!"vctor {c} ..."
   | .vdimExpr _                 => "vdimExpr ..."
   | .vcode _                    => "vcode ..."
+  | .vFlatIntro _               => "vFlatIntro ..."
+  | .vSharpIntro _              => "vSharpIntro ..."
+  | .vShapeIntro _              => "vShapeIntro ..."
 
 def ctermSummary : CTerm → String
   | .var x          => s!"var {x}"
@@ -69,6 +75,12 @@ def ctermSummary : CTerm → String
   | .dimExpr _      => "dimExpr ..."
   | .ctor _ c _ _   => s!"ctor {c} ..."
   | .indElim _ _ _ _ _ => "indElim ..."
+  | .flatIntro _    => "flatIntro ..."
+  | .sharpIntro _   => "sharpIntro ..."
+  | .shapeIntro _   => "shapeIntro ..."
+  | .flatElim _ _   => "flatElim ..."
+  | .sharpElim _ _  => "sharpElim ..."
+  | .shapeElim _ _  => "shapeElim ..."
   | _               => "<other CTerm>"
 
 -- ── Individual test definitions ────────────────────────────────────────────
diff --git a/CubicalTransport/Question.lean b/CubicalTransport/Question.lean
index 4be80e4..8329fa0 100644
--- a/CubicalTransport/Question.lean
+++ b/CubicalTransport/Question.lean
@@ -160,6 +160,22 @@ def IsUnivLine (q : CompQ) : Prop :=
 def IsElLine (q : CompQ) : Prop :=
   q.body.skeleton = SkeletalCType.El
 
+/-- The line is a `.flat` modality.  Encoded via the level-erased
+    skeleton tag. -/
+@[simp]
+def IsFlatLine (q : CompQ) : Prop :=
+  q.body.skeleton = SkeletalCType.flat
+
+/-- The line is a `.sharp` modality. -/
+@[simp]
+def IsSharpLine (q : CompQ) : Prop :=
+  q.body.skeleton = SkeletalCType.sharp
+
+/-- The line is a `.shape` modality. -/
+@[simp]
+def IsShapeLine (q : CompQ) : Prop :=
+  q.body.skeleton = SkeletalCType.shape
+
 -- ── Decidability for the core classifiers ───────────────────────────────────
 -- All instances are computable.  Body-shape predicates are skeleton-eq
 -- forms, decidable via `DecidableEq SkeletalCType`.
@@ -199,6 +215,9 @@ instance instDecidableIsPathLine (q : CompQ) : Decidable (IsPathLine q) := by
     | interval => simp at hs
     | lift A => simp at hs
     | El P => simp at hs
+    | flat A => simp at hs
+    | sharp A => simp at hs
+    | shape A => simp at hs
   · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -217,6 +236,9 @@ instance instDecidableIsGlueLine (q : CompQ) : Decidable (IsGlueLine q) := by
     | interval => simp at hs
     | lift A => simp at hs
     | El P => simp at hs
+    | flat A => simp at hs
+    | sharp A => simp at hs
+    | shape A => simp at hs
   · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -232,6 +254,15 @@ instance (q : CompQ) : Decidable (IsIndLine q) :=
 instance instDecidableIsElLine (q : CompQ) : Decidable (IsElLine q) :=
   inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El))
 
+instance (q : CompQ) : Decidable (IsFlatLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.flat))
+
+instance (q : CompQ) : Decidable (IsSharpLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.sharp))
+
+instance (q : CompQ) : Decidable (IsShapeLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.shape))
+
 -- ── Classifier-conditioned theorems ─────────────────────────────────────────
 
 namespace CompQ
@@ -334,6 +365,12 @@ def IsUnivLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.univ
 
 @[simp]
 def IsElLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.El
+@[simp]
+def IsFlatLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.flat
+@[simp]
+def IsSharpLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.sharp
+@[simp]
+def IsShapeLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.shape
 
 instance (q : TranspQ) : Decidable (IsConstLine q) :=
   inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true))
@@ -356,6 +393,13 @@ instance (q : TranspQ) : Decidable (IsIndLine q) :=
 instance instDecidableTranspIsElLine (q : TranspQ) : Decidable (IsElLine q) :=
   inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El))
 
+instance (q : TranspQ) : Decidable (IsFlatLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.flat))
+instance (q : TranspQ) : Decidable (IsSharpLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.sharp))
+instance (q : TranspQ) : Decidable (IsShapeLine q) :=
+  inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.shape))
+
 instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q) := by
   by_cases hs : q.body.skeleton = SkeletalCType.path
   · obtain ⟨level, env, binder, body, φ, t⟩ := q
@@ -370,6 +414,9 @@ instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q)
     | interval => simp at hs
     | lift A => simp at hs
     | El P => simp at hs
+    | flat A => simp at hs
+    | sharp A => simp at hs
+    | shape A => simp at hs
   · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
@@ -388,6 +435,9 @@ instance instDecidableTranspIsGlueLine (q : TranspQ) : Decidable (IsGlueLine q)
     | interval => simp at hs
     | lift A => simp at hs
     | El P => simp at hs
+    | flat A => simp at hs
+    | sharp A => simp at hs
+    | shape A => simp at hs
   · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_)
     rw [hbody]; rfl
 
diff --git a/CubicalTransport/Readback.lean b/CubicalTransport/Readback.lean
index 1469130..88b7536 100644
--- a/CubicalTransport/Readback.lean
+++ b/CubicalTransport/Readback.lean
@@ -144,6 +144,10 @@ mutual
     | .vdimExpr r => .dimExpr r
     -- Universe-code value: read back as the encoder constructor.
     | .vcode A => .code A
+    -- Modal-introduction values: structural readback of the wrapped value.
+    | .vFlatIntro  a => .flatIntro  (readback a)
+    | .vSharpIntro a => .sharpIntro (readback a)
+    | .vShapeIntro a => .shapeIntro (readback a)
 
   /-- Readback a `CNeu` into a `CTerm`.  Straightforward structural
       recursion: each neutral constructor has a syntactic counterpart.
@@ -172,6 +176,11 @@ mutual
         .indElim S params (readback motive)
           (branches.map (fun p => (p.1, readback p.2)))
           (readbackNeu target)
+    -- Modal-elimination stuck forms: rebuild the elim term with the
+    -- read-back eliminator function and the read-back stuck scrutinee.
+    | .nflatElim  f n => .flatElim  (readback f) (readbackNeu n)
+    | .nsharpElim f n => .sharpElim (readback f) (readbackNeu n)
+    | .nshapeElim f n => .shapeElim (readback f) (readbackNeu n)
 end
 
 -- ── Convenience wrapper ─────────────────────────────────────────────────────
@@ -296,6 +305,28 @@ axiom readback_vpair (a b : CVal) :
 axiom readback_vcode {ℓ : ULevel} (A : CType ℓ) :
     readback (.vcode A) = .code A
 
+-- Modal-introduction readback axioms.
+
+axiom readback_vFlatIntro (a : CVal) :
+    readback (.vFlatIntro a) = .flatIntro (readback a)
+
+axiom readback_vSharpIntro (a : CVal) :
+    readback (.vSharpIntro a) = .sharpIntro (readback a)
+
+axiom readback_vShapeIntro (a : CVal) :
+    readback (.vShapeIntro a) = .shapeIntro (readback a)
+
+-- Modal-elimination (stuck) readback axioms.
+
+axiom readbackNeu_nflatElim (f : CVal) (n : CNeu) :
+    readbackNeu (.nflatElim f n) = .flatElim (readback f) (readbackNeu n)
+
+axiom readbackNeu_nsharpElim (f : CVal) (n : CNeu) :
+    readbackNeu (.nsharpElim f n) = .sharpElim (readback f) (readbackNeu n)
+
+axiom readbackNeu_nshapeElim (f : CVal) (n : CNeu) :
+    readbackNeu (.nshapeElim f n) = .shapeElim (readback f) (readbackNeu n)
+
 axiom readbackNeu_nfst (n : CNeu) :
     readbackNeu (.nfst n) = .fst (readbackNeu n)
 
diff --git a/CubicalTransport/Reflect.lean b/CubicalTransport/Reflect.lean
index 5027ecd..581c012 100644
--- a/CubicalTransport/Reflect.lean
+++ b/CubicalTransport/Reflect.lean
@@ -233,6 +233,18 @@ mutual
         let ℓE ← reflectULevel ℓ
         let PE ← reflectCTerm P
         return mkAppN (mkConst ``CType.El) #[ℓE, PE]
+    | .flat A => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CType.flat) #[ℓE, AE]
+    | .sharp A => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CType.sharp) #[ℓE, AE]
+    | .shape A => do
+        let ℓE ← reflectULevel ℓ
+        let AE ← reflectCType A
+        return mkAppN (mkConst ``CType.shape) #[ℓE, AE]
 
   /-- Reflect a `CTerm` to a `Lean.Expr`. -/
   partial def reflectCTerm : CTerm → MetaM Expr
@@ -315,6 +327,27 @@ mutual
         let ℓE ← reflectULevel ℓ
         let AE ← reflectCType A
         return mkAppN (mkConst ``CTerm.code) #[ℓE, AE]
+    | .flatIntro a => do
+        let ae ← reflectCTerm a
+        return mkApp (mkConst ``CTerm.flatIntro) ae
+    | .sharpIntro a => do
+        let ae ← reflectCTerm a
+        return mkApp (mkConst ``CTerm.sharpIntro) ae
+    | .shapeIntro a => do
+        let ae ← reflectCTerm a
+        return mkApp (mkConst ``CTerm.shapeIntro) ae
+    | .flatElim f m => do
+        let fe ← reflectCTerm f
+        let me ← reflectCTerm m
+        return mkAppN (mkConst ``CTerm.flatElim) #[fe, me]
+    | .sharpElim f m => do
+        let fe ← reflectCTerm f
+        let me ← reflectCTerm m
+        return mkAppN (mkConst ``CTerm.sharpElim) #[fe, me]
+    | .shapeElim f m => do
+        let fe ← reflectCTerm f
+        let me ← reflectCTerm m
+        return mkAppN (mkConst ``CTerm.shapeElim) #[fe, me]
 
   /-- Reflect a `List (Σ ℓ : ULevel, CType ℓ)`.  The Σ pairs are
       built via `mkSigmaULevelCType`; the list is `List.cons`-spine. -/
@@ -764,6 +797,54 @@ mutual
             | some P => return some ⟨ℓ, .El (ℓ := ℓ) P⟩
         else
           return none
+    | (``CType.flat, args) =>
+        -- args = [ℓE, AE]; result level = ℓ (level-preserving modality)
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                let A' : CType ℓ := hA ▸ A
+                return some ⟨ℓ, .flat A'⟩
+              else
+                return none
+        else
+          return none
+    | (``CType.sharp, args) =>
+        -- args = [ℓE, AE]; result level = ℓ
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                let A' : CType ℓ := hA ▸ A
+                return some ⟨ℓ, .sharp A'⟩
+              else
+                return none
+        else
+          return none
+    | (``CType.shape, args) =>
+        -- args = [ℓE, AE]; result level = ℓ
+        if h : args.size = 2 then
+          match ← reifyULevel (args[0]'(by omega)) with
+          | none   => return none
+          | some ℓ =>
+            match ← reifyCType (args[1]'(by omega)) with
+            | none                 => return none
+            | some ⟨ℓ_rec, A⟩ =>
+              if hA : ℓ_rec = ℓ then
+                let A' : CType ℓ := hA ▸ A
+                return some ⟨ℓ, .shape A'⟩
+              else
+                return none
+        else
+          return none
     | _ => return none
 
   /-- Reify a `Lean.Expr` back to a `CTerm`.  Inverts `reflectCTerm`
@@ -1018,6 +1099,59 @@ mutual
                 return none
         else
           return none
+    | (``CTerm.flatIntro, args) =>
+        -- args = [ae]
+        if h : args.size = 1 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some a => return some (.flatIntro a)
+        else
+          return none
+    | (``CTerm.sharpIntro, args) =>
+        if h : args.size = 1 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some a => return some (.sharpIntro a)
+        else
+          return none
+    | (``CTerm.shapeIntro, args) =>
+        if h : args.size = 1 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some a => return some (.shapeIntro a)
+        else
+          return none
+    | (``CTerm.flatElim, args) =>
+        -- args = [fe, me]
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some f =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some m => return some (.flatElim f m)
+        else
+          return none
+    | (``CTerm.sharpElim, args) =>
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some f =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some m => return some (.sharpElim f m)
+        else
+          return none
+    | (``CTerm.shapeElim, args) =>
+        if h : args.size = 2 then
+          match ← reifyCTerm (args[0]'(by omega)) with
+          | none   => return none
+          | some f =>
+            match ← reifyCTerm (args[1]'(by omega)) with
+            | none   => return none
+            | some m => return some (.shapeElim f m)
+        else
+          return none
     | _ => return none
 
   /-- Reify a `Lean.Expr` back to a `List (Σ ℓ : ULevel, CType ℓ)`.
diff --git a/CubicalTransport/Subst.lean b/CubicalTransport/Subst.lean
index d5cabbf..ec49a13 100644
--- a/CubicalTransport/Subst.lean
+++ b/CubicalTransport/Subst.lean
@@ -90,6 +90,10 @@ mutual
     | .interval        => .interval
     | .lift A          => .lift (A.substDim i b)
     | .El P            => .El (P.substDimBool i b)
+    -- Modal type formers: descend into the inner type.
+    | .flat A          => .flat  (A.substDim i b)
+    | .sharp A         => .sharp (A.substDim i b)
+    | .shape A         => .shape (A.substDim i b)
 
   /-- Pointwise `substDim` through a level-heterogeneous list of CType
       parameters.  Each entry's universe level is preserved. -/
@@ -120,6 +124,10 @@ mutual
     | .interval        => .interval
     | .lift A          => .lift (A.substDimExpr i r)
     | .El P            => .El (P.substDim i r)
+    -- Modal type formers: descend into the inner type.
+    | .flat A          => .flat  (A.substDimExpr i r)
+    | .sharp A         => .sharp (A.substDimExpr i r)
+    | .shape A         => .shape (A.substDimExpr i r)
 
   /-- Pointwise `substDimExpr` through a level-heterogeneous list of
       CType parameters. -/
@@ -173,6 +181,15 @@ theorem substDim_lift {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) :
 @[simp] theorem substDim_El {ℓ : ULevel} (i : DimVar) (b : Bool) (P : CTerm) :
     (CType.El (ℓ := ℓ) P).substDim i b = .El (P.substDimBool i b) := rfl
 
+@[simp] theorem substDim_flat {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) :
+    (CType.flat A).substDim i b = .flat (A.substDim i b) := rfl
+
+@[simp] theorem substDim_sharp {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) :
+    (CType.sharp A).substDim i b = .sharp (A.substDim i b) := rfl
+
+@[simp] theorem substDim_shape {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) :
+    (CType.shape A).substDim i b = .shape (A.substDim i b) := rfl
+
 -- ── Reduction lemmas (substDimExpr) ──────────────────────────────────────────
 
 theorem substDimExpr_univ {ℓ : ULevel} (i : DimVar) (r : DimExpr) :
@@ -217,6 +234,15 @@ theorem substDimExpr_lift {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType 
 @[simp] theorem substDimExpr_El {ℓ : ULevel} (i : DimVar) (r : DimExpr) (P : CTerm) :
     (CType.El (ℓ := ℓ) P).substDimExpr i r = .El (P.substDim i r) := rfl
 
+@[simp] theorem substDimExpr_flat {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) :
+    (CType.flat A).substDimExpr i r = .flat (A.substDimExpr i r) := rfl
+
+@[simp] theorem substDimExpr_sharp {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) :
+    (CType.sharp A).substDimExpr i r = .sharp (A.substDimExpr i r) := rfl
+
+@[simp] theorem substDimExpr_shape {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) :
+    (CType.shape A).substDimExpr i r = .shape (A.substDimExpr i r) := rfl
+
 -- ── Bool endpoint = DimExpr at canonical endpoint ────────────────────────────
 
 mutual
@@ -270,6 +296,15 @@ mutual
         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]
+    | .flat A => by
+        show CType.flat (A.substDim i b) = CType.flat (A.substDimExpr i _)
+        rw [substDim_eq_substDimExpr i b A]
+    | .sharp A => by
+        show CType.sharp (A.substDim i b) = CType.sharp (A.substDimExpr i _)
+        rw [substDim_eq_substDimExpr i b A]
+    | .shape A => by
+        show CType.shape (A.substDim i b) = CType.shape (A.substDimExpr i _)
+        rw [substDim_eq_substDimExpr i b A]
 
   /-- 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 4314de4..69414be 100644
--- a/CubicalTransport/Syntax.lean
+++ b/CubicalTransport/Syntax.lean
@@ -140,6 +140,32 @@ mutual
         propositions and refer back to the underlying type. -/
     | El {ℓ : ULevel} (P : CTerm)
         : CType ℓ
+    /-- **Modal type former: flat (♭).**  Given `A : CType ℓ`, the type
+        `flat A` lives at the same universe level `ℓ`.  Together with
+        `sharp` and `shape`, these are the three modalities of the
+        cohesive triple `♭ ⊣ ♯ ⊣ ʃ` (Schreiber/Shulman cohesive HoTT).
+
+        At the engine layer we add the data constructor; the modal
+        cohesion content (Crisp variables, the `♭ ⊣ ♯` adjunction,
+        modal-shape commutation diagrams) is the Phase 3 module.
+
+        Per THEORY.md §3.1; mirrors `path` in level preservation. -/
+    | flat  {ℓ : ULevel} (A : CType ℓ)
+        : CType ℓ
+    /-- **Modal type former: sharp (♯).**  Given `A : CType ℓ`, the type
+        `sharp A` lives at the same universe level `ℓ`.  Right adjoint
+        of `flat` in the cohesive triple `♭ ⊣ ♯ ⊣ ʃ`.
+
+        Per THEORY.md §3.1. -/
+    | sharp {ℓ : ULevel} (A : CType ℓ)
+        : CType ℓ
+    /-- **Modal type former: shape (ʃ).**  Given `A : CType ℓ`, the type
+        `shape A` lives at the same universe level `ℓ`.  Left adjoint
+        of `flat` in the cohesive triple `♭ ⊣ ♯ ⊣ ʃ`.
+
+        Per THEORY.md §3.1. -/
+    | shape {ℓ : ULevel} (A : CType ℓ)
+        : CType ℓ
 
   /-- Terms in the cubical calculus.  Un-indexed by universe level —
       the level discipline lives in the typing judgment (`HasType`,
@@ -198,6 +224,36 @@ mutual
         `.univ (ℓ := ℓ)`.  Carries the underlying type as data. -/
     | code {ℓ : ULevel} (A : CType ℓ)
         : CTerm
+    /-- **Modal introduction: η_♭ (flat).**  Given `a : A`, the term
+        `flatIntro a` inhabits `flat A`.  Mirrors the `glueIn` shape:
+        a single argument carrying the wrapped value.
+
+        Reduction: `flatElim f (flatIntro a)` ↝ `app f a`. -/
+    | flatIntro  (a : CTerm)
+        : CTerm
+    /-- **Modal introduction: η_♯ (sharp).**  Given `a : A`, the term
+        `sharpIntro a` inhabits `sharp A`. -/
+    | sharpIntro (a : CTerm)
+        : CTerm
+    /-- **Modal introduction: η_ʃ (shape).**  Given `a : A`, the term
+        `shapeIntro a` inhabits `shape A`. -/
+    | shapeIntro (a : CTerm)
+        : CTerm
+    /-- **Modal elimination: ♭.rec.**  Given the elimination function
+        `f : A → C` and a scrutinee `m : flat A`, produce a term of
+        type `C`.  Two CTerms: target then scrutinee — same shape as
+        `unglue` (modulo unglue's leading FaceFormula).
+
+        Reduction: `flatElim f (flatIntro a)` ↝ `app f a` (β-rule).
+        Otherwise: stuck `nflatElim` neutral. -/
+    | flatElim   (f m : CTerm)
+        : CTerm
+    /-- **Modal elimination: ♯.rec.**  Same shape as `flatElim`. -/
+    | sharpElim  (f m : CTerm)
+        : CTerm
+    /-- **Modal elimination: ʃ.rec.**  Same shape as `flatElim`. -/
+    | shapeElim  (f m : CTerm)
+        : CTerm
 
   /-- Argument shape for a schema constructor (REL1, §2.1). -/
   inductive CTypeArg where
@@ -268,6 +324,9 @@ inductive SkeletalCType : Type where
   | interval
   | lift
   | El
+  | flat
+  | sharp
+  | shape
   deriving Repr, DecidableEq
 
 /-- Strip the universe index, preserving the head constructor as a tag.
@@ -284,6 +343,9 @@ def CType.skeleton {ℓ : ULevel} : CType ℓ → SkeletalCType
   | .interval      => .interval
   | .lift  _       => .lift
   | .El _          => .El
+  | .flat  _       => .flat
+  | .sharp _       => .sharp
+  | .shape _       => .shape
 
 -- ── Skeleton equations (rfl-provable) ────────────────────────────────────────
 
@@ -353,6 +415,21 @@ theorem CType.skeleton_lift {ℓ : ULevel} (A : CType ℓ) :
 @[simp] theorem CType.skeleton_El {ℓ : ULevel} (P : CTerm) :
     (CType.El (ℓ := ℓ) P).skeleton = SkeletalCType.El := rfl
 
+/-- The skeleton of `.flat` is `.flat`. -/
+@[simp]
+theorem CType.skeleton_flat {ℓ : ULevel} (A : CType ℓ) :
+    (CType.flat A).skeleton = SkeletalCType.flat := rfl
+
+/-- The skeleton of `.sharp` is `.sharp`. -/
+@[simp]
+theorem CType.skeleton_sharp {ℓ : ULevel} (A : CType ℓ) :
+    (CType.sharp A).skeleton = SkeletalCType.sharp := rfl
+
+/-- The skeleton of `.shape` is `.shape`. -/
+@[simp]
+theorem CType.skeleton_shape {ℓ : ULevel} (A : CType ℓ) :
+    (CType.shape A).skeleton = SkeletalCType.shape := rfl
+
 -- ── Constructor disjointness via skeleton ────────────────────────────────────
 
 /-- Skeletons of distinct constructors are distinct.  This is the
@@ -436,6 +513,15 @@ mutual
     -- Universe-code constructor: `code A` carries a CType payload.
     -- Same approximation as transp/comp: A is not recursed into.
     | .code A           => .code A
+    -- Modal introductions: structural recursion into the wrapped term.
+    | .flatIntro a      => .flatIntro (a.substDim i r)
+    | .sharpIntro a     => .sharpIntro (a.substDim i r)
+    | .shapeIntro a     => .shapeIntro (a.substDim i r)
+    -- Modal eliminations: structural recursion into both subterms
+    -- (eliminator function and scrutinee).
+    | .flatElim f m     => .flatElim (f.substDim i r) (m.substDim i r)
+    | .sharpElim f m    => .sharpElim (f.substDim i r) (m.substDim i r)
+    | .shapeElim f m    => .shapeElim (f.substDim i r) (m.substDim i r)
 
   /-- 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/Typing.lean b/CubicalTransport/Typing.lean
index d8366a2..31c437f 100644
--- a/CubicalTransport/Typing.lean
+++ b/CubicalTransport/Typing.lean
@@ -173,6 +173,53 @@ inductive HasType : Ctx → CTerm → ∀ {ℓ : ULevel}, CType ℓ → Prop whe
   | code  : ∀ {Γ : Ctx} {ℓ : ULevel} (A : CType ℓ),
             HasType Γ (.code A) (.univ (ℓ := ℓ))
 
+  /-- **Modal introduction (flat).**  Given `a : A`, the term
+      `flatIntro a` inhabits `flat A`.  Engine-layer rule —
+      modal-cohesion contextual restrictions (Crisp variables,
+      Π-modality interaction, etc.) land in Phase 3. -/
+  | flatIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
+      HasType Γ a A →
+      HasType Γ (.flatIntro a) (.flat A)
+
+  /-- **Modal introduction (sharp).** -/
+  | sharpIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
+      HasType Γ a A →
+      HasType Γ (.sharpIntro a) (.sharp A)
+
+  /-- **Modal introduction (shape).** -/
+  | shapeIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} :
+      HasType Γ a A →
+      HasType Γ (.shapeIntro a) (.shape A)
+
+  /-- **Modal elimination (flat).**  Given an eliminator `f : A → C`
+      and a scrutinee `m : flat A`, produce a term of type `C`.
+
+      Engine layer: this is the bare recursion-principle shape; the
+      modal-cohesion side-conditions (e.g. C must be flat-modal for
+      the elim to be well-formed in cohesive HoTT) are deferred to
+      Phase 3 (`Modal.lean`).  At the engine layer the rule reflects
+      the recursion principle directly so that `eval` and `readback`
+      can dispatch on it. -/
+  | flatElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
+             {f m : CTerm} {var : String} :
+      HasType Γ f (.pi var A C) →
+      HasType Γ m (.flat A) →
+      HasType Γ (.flatElim f m) C
+
+  /-- **Modal elimination (sharp).** -/
+  | sharpElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
+              {f m : CTerm} {var : String} :
+      HasType Γ f (.pi var A C) →
+      HasType Γ m (.sharp A) →
+      HasType Γ (.sharpElim f m) C
+
+  /-- **Modal elimination (shape).** -/
+  | shapeElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'}
+              {f m : CTerm} {var : String} :
+      HasType Γ f (.pi var A C) →
+      HasType Γ m (.shape A) →
+      HasType Γ (.shapeElim f m) C
+
 -- ── Structural rules ──────────────────────────────────────────────────────────
 
 /-- Core: insert (x, B) into context Γ between a prefix Γ₁ and suffix Γ₂.
@@ -227,6 +274,24 @@ private theorem HasType.weaken_core
       intro _ _; exact HasType.dimExpr
   | code A =>
       intro _ _; exact HasType.code A
+  | flatIntro ha ih =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.flatIntro (ih Γ₁ rfl)
+  | sharpIntro ha ih =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.sharpIntro (ih Γ₁ rfl)
+  | shapeIntro ha ih =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.shapeIntro (ih Γ₁ rfl)
+  | flatElim hf hm ihf ihm =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.flatElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
+  | sharpElim hf hm ihf ihm =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.sharpElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
+  | shapeElim hf hm ihf ihm =>
+      intro Γ₁ hΓ; subst hΓ
+      exact HasType.shapeElim (ihf Γ₁ rfl) (ihm Γ₁ rfl)
 
 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 08e7865..e55c724 100644
--- a/CubicalTransport/Value.lean
+++ b/CubicalTransport/Value.lean
@@ -81,6 +81,13 @@ mutual
     | vdimExpr : DimExpr → CVal
     /-- Value form of `CTerm.code A`.  Carries the encoded CType. -/
     | vcode {ℓ : ULevel} : CType ℓ → CVal
+    /-- Value form of `CTerm.flatIntro a`: the η-introduction value
+        for the flat (♭) modality, carrying the wrapped value. -/
+    | vFlatIntro  : CVal → CVal
+    /-- Value form of `CTerm.sharpIntro a`. -/
+    | vSharpIntro : CVal → CVal
+    /-- Value form of `CTerm.shapeIntro a`. -/
+    | vShapeIntro : CVal → CVal
 
   /-- Neutral (stuck) terms. -/
   inductive CNeu : Type where
@@ -116,6 +123,14 @@ mutual
     /-- A stuck inductive eliminator (REL1).  `params` is level-heterogeneous. -/
     | nIndElim : CTypeSchema → List (Σ ℓ : ULevel, CType ℓ) → CVal →
                  List (String × CVal) → CNeu → CNeu
+    /-- A stuck flat-modality eliminator: `flatElim f m` where the
+        scrutinee `m` is a stuck CNeu (so β can't fire).  Stores the
+        evaluated eliminator function and the stuck scrutinee. -/
+    | nflatElim  : CVal → CNeu → CNeu
+    /-- A stuck sharp-modality eliminator. -/
+    | nsharpElim : CVal → CNeu → CNeu
+    /-- A stuck shape-modality eliminator. -/
+    | nshapeElim : CVal → CNeu → CNeu
 end
 
 -- Inhabited instances — needed so `partial def` evaluators can be elaborated