diff --git a/.github/workflows/web-demos.yml b/.github/workflows/web-demos.yml
index e7b9c6f8..6979b250 100644
--- a/.github/workflows/web-demos.yml
+++ b/.github/workflows/web-demos.yml
@@ -13,99 +13,98 @@ concurrency:
   group: web-demos-${{ github.event_name }}-${{ github.event.pull_request.number || github.ref }}
   cancel-in-progress: true
 
-# jobs:
-#   build-and-deploy:
-#     runs-on: ubuntu-latest
-#     env:
-#       CARGO_TARGET_DIR: ${{ github.workspace }}/target
-#       NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-#       NETLIFY_SITE_ID: ${{ secrets.NETLIFY_SITE_ID }}
+jobs:
+  # build-and-deploy:
+  #   runs-on: ubuntu-latest
+  #   env:
+  #     CARGO_TARGET_DIR: ${{ github.workspace }}/target
+  #     NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
+  #     NETLIFY_SITE_ID: ${{ secrets.NETLIFY_SITE_ID }}
 
-#     steps:
-#       - name: Checkout ⬇️
-#         uses: actions/checkout@v6
+  #   steps:
+  #     - name: Checkout ⬇️
+  #       uses: actions/checkout@v6
 
-#       - name: Install Nix ❄️
-#         uses: cachix/install-nix-action@v31
+  #     - name: Install Nix ❄️
+  #       uses: cachix/install-nix-action@v31
 
-#       - name: Set up Cachix ♻️
-#         if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
-#         uses: cachix/cachix-action@v17
-#         with:
-#           name: coln
-#           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+  #     - name: Set up Cachix ♻️
+  #       if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
+  #       uses: cachix/cachix-action@v17
+  #       with:
+  #         name: coln
+  #         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
 
-#       - name: Restore build caches
-#         uses: actions/cache@v4
-#         with:
-#           path: |
-#             .pnpm-store
-#             ~/.npm
-#             ~/.cargo/registry
-#             ~/.cargo/git
-#             ~/.ghc-wasm/.cabal
-#             target
-#             dist-newstyle
-#           key: web-demos-${{ runner.os }}-${{ hashFiles('flake.lock', 'Cargo.lock', 'cabal.project', 'packages/**/*.cabal', 'packages/coln-js-runtime/package-lock.json', 'examples/sync-demo/pnpm-lock.yaml') }}
-#           restore-keys: |
-#             web-demos-${{ runner.os }}-
+  #     - name: Restore build caches
+  #       uses: actions/cache@v4
+  #       with:
+  #         path: |
+  #           .pnpm-store
+  #           ~/.npm
+  #           ~/.cargo/registry
+  #           ~/.cargo/git
+  #           ~/.ghc-wasm/.cabal
+  #           target
+  #           dist-newstyle
+  #         key: web-demos-${{ runner.os }}-${{ hashFiles('flake.lock', 'Cargo.lock', 'cabal.project', 'packages/**/*.cabal', 'packages/coln-js-runtime/package-lock.json', 'examples/sync-demo/pnpm-lock.yaml') }}
+  #         restore-keys: |
+  #           web-demos-${{ runner.os }}-
 
-#       - name: Build sync demo
-#         run: nix run --accept-flake-config .#sync-demo -- "$GITHUB_WORKSPACE"
-#         env:
-#           VITE_BASE: /sync/
+  #     - name: Build sync demo
+  #       run: nix run --accept-flake-config .#sync-demo -- "$GITHUB_WORKSPACE"
+  #       env:
+  #         VITE_BASE: /sync/
 
-#       - name: Build web compiler
-#         run: |
-#           nix develop --accept-flake-config --command wasm32-wasi-cabal update 'hackage.haskell.org,2026-07-15T17:07:49Z'
-#           nix develop --accept-flake-config --command just examples/build-web-compiler
+  #     - name: Build web compiler
+  #       run: |
+  #         nix develop --accept-flake-config --command wasm32-wasi-cabal update 'hackage.haskell.org,2026-07-15T17:07:49Z'
+  #         nix develop --accept-flake-config --command just examples/build-web-compiler
 
-#       - name: Assemble deploy directory
-#         run: |
-#           cp examples/index.html examples/style.css _build/web/
-#           cp -r examples/sync-demo/dist _build/web/sync
+  #     - name: Assemble deploy directory
+  #       run: |
+  #         cp examples/index.html examples/style.css _build/web/
+  #         cp -r examples/sync-demo/dist _build/web/sync
 
-#       - name: Deploy PR preview to Netlify
-#         id: deploy-preview
-#         if: github.event_name == 'pull_request' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
-#         run: |
-#           npx --yes netlify-cli@latest deploy \
-#             --auth "$NETLIFY_AUTH_TOKEN" \
-#             --site "$NETLIFY_SITE_ID" \
-#             --dir _build/web \
-#             --no-build \
-#             --alias "pr-${{ github.event.pull_request.number }}" \
-#             --message "PR #${{ github.event.pull_request.number }} web demos" \
-#             --json > netlify-deploy.json
+  #     - name: Deploy PR preview to Netlify
+  #       id: deploy-preview
+  #       if: github.event_name == 'pull_request' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
+  #       run: |
+  #         npx --yes netlify-cli@latest deploy \
+  #           --auth "$NETLIFY_AUTH_TOKEN" \
+  #           --site "$NETLIFY_SITE_ID" \
+  #           --dir _build/web \
+  #           --no-build \
+  #           --alias "pr-${{ github.event.pull_request.number }}" \
+  #           --message "PR #${{ github.event.pull_request.number }} web demos" \
+  #           --json > netlify-deploy.json
 
-#           cat netlify-deploy.json
-#           deploy_url=$(node -e "const d = require('./netlify-deploy.json'); console.log(d.deploy_ssl_url || d.ssl_url || d.deploy_url || d.url)")
-#           echo "deploy-url=$deploy_url" >> "$GITHUB_OUTPUT"
+  #         cat netlify-deploy.json
+  #         deploy_url=$(node -e "const d = require('./netlify-deploy.json'); console.log(d.deploy_ssl_url || d.ssl_url || d.deploy_url || d.url)")
+  #         echo "deploy-url=$deploy_url" >> "$GITHUB_OUTPUT"
 
-#       - name: Comment with deploy preview URL
-#         if: github.event_name == 'pull_request' && steps.deploy-preview.outputs.deploy-url != ''
-#         uses: actions/github-script@v8
-#         with:
-#           script: |
-#             const marker = '<!-- coln-web-demos-deploy-preview -->'
-#             const body = `${marker}\nWeb demo preview: ${{ steps.deploy-preview.outputs.deploy-url }}`
-#             const { owner, repo } = context.repo
-#             const issue_number = context.issue.number
-#             const comments = await github.rest.issues.listComments({ owner, repo, issue_number, per_page: 100 })
-#             const existing = comments.data.find(comment => comment.body?.includes(marker))
-#             if (existing) {
-#               await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body })
-#             } else {
-#               await github.rest.issues.createComment({ owner, repo, issue_number, body })
-#             }
-
-#       - name: Deploy main to Netlify production
-#         if: github.event_name == 'push' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
-#         run: |
-#           npx --yes netlify-cli@latest deploy \
-#             --auth "$NETLIFY_AUTH_TOKEN" \
-#             --site "$NETLIFY_SITE_ID" \
-#             --dir _build/web \
-#             --no-build \
-#             --prod \
-#             --message "web demos ${{ github.sha }}"
+  #     - name: Comment with deploy preview URL
+  #       if: github.event_name == 'pull_request' && steps.deploy-preview.outputs.deploy-url != ''
+  #       uses: actions/github-script@v8
+  #       with:
+  #         script: |
+  #           const marker = '<!-- coln-web-demos-deploy-preview -->'
+  #           const body = `${marker}\nWeb demo preview: ${{ steps.deploy-preview.outputs.deploy-url }}`
+  #           const { owner, repo } = context.repo
+  #           const issue_number = context.issue.number
+  #           const comments = await github.rest.issues.listComments({ owner, repo, issue_number, per_page: 100 })
+  #           const existing = comments.data.find(comment => comment.body?.includes(marker))
+  #           if (existing) {
+  #             await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body })
+  #           } else {
+  #             await github.rest.issues.createComment({ owner, repo, issue_number, body })
+  #           }
+  #     - name: Deploy main to Netlify production
+  #       if: github.event_name == 'push' && env.NETLIFY_AUTH_TOKEN != '' && env.NETLIFY_SITE_ID != ''
+  #       run: |
+  #         npx --yes netlify-cli@latest deploy \
+  #           --auth "$NETLIFY_AUTH_TOKEN" \
+  #           --site "$NETLIFY_SITE_ID" \
+  #           --dir _build/web \
+  #           --no-build \
+  #           --prod \
+  #           --message "web demos ${{ github.sha }}"
diff --git a/manual/templates/plain.tree b/manual/templates/plain.tree
new file mode 100644
index 00000000..e69de29b
diff --git a/manual/trees/0001.tree b/manual/trees/0001.tree
index 38184706..d6d04343 100644
--- a/manual/trees/0001.tree
+++ b/manual/trees/0001.tree
@@ -2,9 +2,11 @@
 
 \p{Coln is a database with an expressive language for schemas, queries, and migrations. This document forms the manual for Coln.}
 
-\transclude{002H}
-\transclude{0002}
-\transclude{000K}
-\transclude{000L}
-\transclude{000M}
-\transclude{0003}
+\ol{
+  \li{[[002H]]}
+  \li{[[0002]]}
+  \li{[[000K]]}
+  \li{[[000L]]}
+  \li{[[000M]]}
+  \li{[[0003]]}
+}
diff --git a/manual/trees/0002.tree b/manual/trees/0002.tree
index 3e4ac337..31903d18 100644
--- a/manual/trees/0002.tree
+++ b/manual/trees/0002.tree
@@ -72,8 +72,4 @@
 
 \transclude{000B}
 
-\subtree[000I]{
-  \title{Organization}
-
-  \p{}
-}
+\transclude{000I}
diff --git a/manual/trees/000I.tree b/manual/trees/000I.tree
new file mode 100644
index 00000000..082e2790
--- /dev/null
+++ b/manual/trees/000I.tree
@@ -0,0 +1,3 @@
+\title{Organization}
+
+\p{}
diff --git a/manual/trees/002K.tree b/manual/trees/002K.tree
new file mode 100644
index 00000000..f54be495
--- /dev/null
+++ b/manual/trees/002K.tree
@@ -0,0 +1 @@
+\title{Developer documentation}
diff --git a/packages/coln-compiler/coln-compiler.cabal b/packages/coln-compiler/coln-compiler.cabal
index d2817239..763c7318 100644
--- a/packages/coln-compiler/coln-compiler.cabal
+++ b/packages/coln-compiler/coln-compiler.cabal
@@ -30,6 +30,7 @@ library
     Coln.Core.Syntax
     Coln.Core.Value
     Coln.Diagnostics
+    Coln.Elaborator.Coercion
     Coln.Elaborator.Debug
     Coln.Elaborator.Diagnostics
     Coln.Elaborator.Environment
@@ -37,12 +38,16 @@ library
     Coln.Elaborator.Rules.Builtin
     Coln.Elaborator.Rules.Equality
     Coln.Elaborator.Rules.Function
+    Coln.Elaborator.Rules.Initial
+    Coln.Elaborator.Rules.Polarity
     Coln.Elaborator.Rules.Record
     Coln.Elaborator.Rules.Universe
     Coln.Elaborator.Rules.Variable
     Coln.Frontend.Diagnostics
     Coln.Frontend.Notation
     Coln.Frontend.Parser
+    Coln.Frontend.Parser.Expr
+    Coln.Frontend.Parser.Top
     Coln.Report
 
   hs-source-dirs: src
diff --git a/packages/coln-compiler/src/Coln/Backend/Lower.hs b/packages/coln-compiler/src/Coln/Backend/Lower.hs
index 4dceb3fa..df1ebdfd 100644
--- a/packages/coln-compiler/src/Coln/Backend/Lower.hs
+++ b/packages/coln-compiler/src/Coln/Backend/Lower.hs
@@ -73,6 +73,7 @@ instance Lower (V.El N) Term where
   lower :: CtxLen -> V.El N -> Term
   lower n = \case
     V.Neu ne -> lower n ne
+    V.InitNeu _ -> panic "can't lower init yet"
     V.Code _ -> panic "non set-level term"
     V.Lam _ _ -> panic "non set-level term"
     V.Cons ds -> Cons (lower n <$> ds)
@@ -99,6 +100,7 @@ separate n = \case
       let (shapes, props) = unzip $ go rt.capture (toList rt.fieldTypes)
       Ty (Tuple (withHead rt.fieldTypes shapes)) (And (withHead rt.fieldTypes props))
     Nothing -> panic "lowering neutral type"
+  V.InitDecode _ -> panic "can't lower init yet"
   V.Function _ -> panic "lowering non-set-level type: Function"
   V.Eq et -> \_ -> Ty Unit (Equal (lower n et.lhs) (lower n et.rhs))
   V.BuiltinTy t -> \_ -> Ty (BuiltinTy t) PTrue
diff --git a/packages/coln-compiler/src/Coln/Backend/TypeScript/Generate.hs b/packages/coln-compiler/src/Coln/Backend/TypeScript/Generate.hs
index 3c86fcb5..ab2a4451 100644
--- a/packages/coln-compiler/src/Coln/Backend/TypeScript/Generate.hs
+++ b/packages/coln-compiler/src/Coln/Backend/TypeScript/Generate.hs
@@ -117,6 +117,7 @@ genEntryModule imports a ev = go 0 a ev
           case V.ebind V.decode ev' of
             V.Become a -> TS.DTypeDef $ genTypeDef access n a
             V.Describe a -> TS.DInterface $ genInterface access n a
+            V.BecomeWith _ -> panic "can't lower becomewith yet"
     Just $ TS.Module imports (TS.Exported <$> definitions)
   go n (V.Function ft) ev' = do
     let v = V.local (FId n) ft.dom
@@ -172,6 +173,7 @@ argName _ (V.CloConst _) = panic "closures from the layout process should have a
 genEl :: Access -> TSCtxShape -> V.El N -> TS.El
 genEl access cs = \case
   V.Neu n -> genSp cs n.spine $ genHead access cs n.head
+  V.InitNeu _ -> panic "can't lower init yet"
   V.Code a -> genTyVal access cs a
   V.Lam dom clo -> do
     let v = V.local (FId cs.len) dom
diff --git a/packages/coln-compiler/src/Coln/Core/Conversion.hs b/packages/coln-compiler/src/Coln/Core/Conversion.hs
index 5ca80c0c..a7184b70 100644
--- a/packages/coln-compiler/src/Coln/Core/Conversion.hs
+++ b/packages/coln-compiler/src/Coln/Core/Conversion.hs
@@ -62,6 +62,9 @@ instance DefEq (V.Ty N) where
     V.Decode n -> case a' of
       V.Decode n' -> defEq cs n n'
       _ -> throwUnequalTys cs a a' Nothing
+    V.InitDecode n -> case a' of
+      V.InitDecode n' -> defEq cs n n'
+      _ -> throwUnequalTys cs a a' Nothing
     V.Function f -> case a' of
       V.Function f' -> do
         unless (f.variant == f'.variant) $
@@ -123,6 +126,9 @@ instance DefEq V.DecodedNeutral where
 instance DefEq V.Neutral where
   defEq cs n n' = defEq cs (V.toBare n) (V.toBare n')
 
+instance DefEq V.InitNeutral where
+  defEq cs n n' = defEq cs (V.fullNeu n) (V.fullNeu n')
+
 canon :: V.El N -> V.El N
 canon v@(V.Neu n) = case V.behavior n.ty of
   V.LikeRecord _ -> V.Cons (V.unwrap n.expansion)
@@ -137,6 +143,9 @@ instance DefEq (V.El N) where
     V.Neu n -> case canon v' of
       V.Neu n' -> defEq cs n n'
       _ -> throwUnequalEls cs v v' Nothing
+    V.InitNeu n -> case canon v' of
+      V.InitNeu n' -> defEq cs n n'
+      _ -> throwUnequalEls cs v v' Nothing
     V.Code a -> case canon v' of
       V.Code a' -> defEq cs a a'
       _ -> throwUnequalEls cs v v' Nothing
diff --git a/packages/coln-compiler/src/Coln/Core/Evaluation.hs b/packages/coln-compiler/src/Coln/Core/Evaluation.hs
index 4ee38f13..d5bdab05 100644
--- a/packages/coln-compiler/src/Coln/Core/Evaluation.hs
+++ b/packages/coln-compiler/src/Coln/Core/Evaluation.hs
@@ -43,6 +43,9 @@ instance Compile S.El V.El where
     S.Proj t x -> do
       let k = compile t
       \vs -> V.proj (k vs) x
+    S.Init t -> do
+      let k = compile t
+      \vs -> V.BecomeWith $ \n -> V.InitNeu (V.InitNeutral n (k vs) V.Id)
     S.Lit l -> \_ -> V.Lit l
     S.Is t -> do
       let k = compile t
diff --git a/packages/coln-compiler/src/Coln/Core/Globals.hs b/packages/coln-compiler/src/Coln/Core/Globals.hs
index e6946b05..907d739a 100644
--- a/packages/coln-compiler/src/Coln/Core/Globals.hs
+++ b/packages/coln-compiler/src/Coln/Core/Globals.hs
@@ -17,6 +17,7 @@ data GlobalEntry = GlobalEntry
   { syn :: S.El D
   , val :: V.El N
   , ty :: V.Ty N
+  , mode :: Mode
   }
 
 data Globals = Globals
diff --git a/packages/coln-compiler/src/Coln/Core/Layout.hs b/packages/coln-compiler/src/Coln/Core/Layout.hs
index 387630db..e43ffcb3 100644
--- a/packages/coln-compiler/src/Coln/Core/Layout.hs
+++ b/packages/coln-compiler/src/Coln/Core/Layout.hs
@@ -71,7 +71,7 @@ layout p sc a
         let a = V.EltOf (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
         (gt, M.code (M.fromVTy sc.len a))
       V.NoRules -> panic "cannot layout type with no rules"
-      V.LikeBuiltinTy _; V.LikeU _ -> panic "non-theory type"
+      V.LikeBuiltinTy _; V.LikeU _; V.LikeInductive _ -> panic "non-theory type"
   | (levelOf a).mlevel == Set = do
       let gt = Leaf (Fun (toList sc.names) (toList sc.ctx) (readb sc.len a))
       let v = V.tableLookup (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound)) a
diff --git a/packages/coln-compiler/src/Coln/Core/Memoed.hs b/packages/coln-compiler/src/Coln/Core/Memoed.hs
index 7da6002e..a492e0e7 100644
--- a/packages/coln-compiler/src/Coln/Core/Memoed.hs
+++ b/packages/coln-compiler/src/Coln/Core/Memoed.hs
@@ -30,6 +30,7 @@ class Core el ty | el -> ty, ty -> el where
   lam :: (V.HasEvaluation c) => V.Locals -> ty N -> S.Abs el c -> el c
   cons :: (V.HasEvaluation c) => Dict (el c) -> el c
   proj :: el N -> Name -> el N
+  init :: ty N -> el D
   lit :: Literal -> el N
   is :: el N -> el D
   univ :: Universe -> ty N
@@ -55,6 +56,8 @@ instance Core El Ty where
       (V.epure $ V.Lam dom.val (V.CloConst body.val))
   cons d = M (S.Cons $ (.stx) <$> d) (V.epure $ V.Cons $ (.val) <$> d)
   proj x f = M (S.Proj x.stx f) (V.proj x.val f)
+  init a =
+    M (S.Init a.stx) (V.BecomeWith $ \n -> V.InitNeu (V.InitNeutral n a.val V.Id))
   lit l = M (S.Lit l) (V.Lit l)
   is x = M (S.Is x.stx) (V.Become x.val)
   univ u = M (S.U u) (V.U u)
@@ -90,11 +93,13 @@ instance (V.HasEvaluation c) => LevelOf (Ty c) where
     SDescriptive -> case ty.val of
       V.Describe ty' -> levelOf ty'
       V.Become ty' -> levelOf ty'
+      -- This is kind of a hack, but shouldn't appear in practice in any case
+      V.BecomeWith f -> levelOf (f $ V.BareNeutral (V.LocalVar (FId 0)) V.Id)
 
 instance Readback (Memoed a b c) (a c) where
   readb _ m = m.stx
 
-mkGlobal :: Name -> V.Ty N -> El D -> GlobalEntry
-mkGlobal n ty x = do
+mkGlobal :: Name -> V.Ty N -> El D -> Mode -> GlobalEntry
+mkGlobal n ty x m = do
   let neu = V.reflect (V.GlobalVar n neu) V.Id ty (Just x.val)
-  GlobalEntry x.stx neu ty
+  GlobalEntry x.stx neu ty m
diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 93913b81..3a5655a9 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -109,7 +109,11 @@ functionMLevelFor v1 v2 = case (v1, v2) of
   (Theory, _) -> pure TheoryTop
   (Top, _) -> Nothing
 
-data FunctionVariant = FunctionVariant {mlevel :: FunctionVariantMLevel, hlevel :: HLevel}
+data FunctionVariant = FunctionVariant
+  { mlevel :: FunctionVariantMLevel
+  , hlevel :: HLevel
+  , domainMode :: Mode
+  }
   deriving (Eq, Show)
 
 instance Pretty FunctionVariant where
@@ -183,3 +187,12 @@ data TableName = TableName {realm :: RealmId, path :: Path}
 
 instance DPretty TableName where
   dpretty tn = concatWith (surround dot) (dpretty <$> toList tn.path)
+
+-- Mode
+--------------------------------------------------------------------------------
+
+data Mode = Inductive | Conjunctive
+  deriving (Show, Eq, Ord)
+
+instance DPretty Mode where
+  dpretty = pretty . show
diff --git a/packages/coln-compiler/src/Coln/Core/Print.hs b/packages/coln-compiler/src/Coln/Core/Print.hs
index 365df236..dbf6f34a 100644
--- a/packages/coln-compiler/src/Coln/Core/Print.hs
+++ b/packages/coln-compiler/src/Coln/Core/Print.hs
@@ -55,6 +55,7 @@ instance ToNotation (El e) where
       N.Tuple [field y t | (y, t) <- toList d] ()
      where
       field y t = N.Infix (N.Ident y ()) (N.Keyword ":=" ()) (toNotation xs t)
+    Init t -> N.Juxt (N.Keyword "init" ()) (toNotation xs t)
     Lit (LitInt i) -> N.Int i ()
     Lit (LitString s) -> N.String s ()
     Is t -> toNotation xs t -- invisible
@@ -102,6 +103,7 @@ instance ToNotation TypeBehavior where
     LikeFunction ft -> toNotation xs (Function ft)
     LikeRecord rt -> toNotation xs (Record rt)
     LikeBuiltinTy bt -> toNotation xs (BuiltinTy bt)
+    LikeInductive t -> toNotation xs t
     NoRules -> N.Keyword "NoRules" ()
 
 toNotationTele :: [Name] -> [Ty N] -> [N.Ntn0]
diff --git a/packages/coln-compiler/src/Coln/Core/Readback.hs b/packages/coln-compiler/src/Coln/Core/Readback.hs
index 42953090..2b720af5 100644
--- a/packages/coln-compiler/src/Coln/Core/Readback.hs
+++ b/packages/coln-compiler/src/Coln/Core/Readback.hs
@@ -36,6 +36,8 @@ instance Readback (V.Description V.El) (S.El D) where
   readb n = \case
     V.Describe v -> readb n v
     V.Become v -> S.Is (readb n v)
+    V.BecomeWith f ->
+      S.Is (readb (n + 1) (f (V.BareNeutral (V.LocalVar (FId n)) V.Id)))
 
 readbClo :: (Readback (V.Evaluation a c) (b c)) => CtxLen -> V.Ty N -> V.Clo a c -> S.Abs b c
 readbClo n dom = \case
@@ -45,6 +47,7 @@ readbClo n dom = \case
 instance (V.HasEvaluation c) => Readback (V.El c) (S.El c) where
   readb n = \case
     V.Neu ne -> readb n ne.spine $ readb n ne.head
+    V.InitNeu ne -> readb n ne.spine $ readb n ne.name
     V.Code a -> S.Code (readb n a)
     V.Lam dom body -> S.Lam (readb n dom) $ case V.scase @c of
       SNominative -> readbClo n dom body
@@ -92,6 +95,7 @@ instance (V.HasEvaluation c) => Readback (V.Ty c) (S.Ty c) where
   readb n = \case
     V.U u -> S.U u
     V.Decode ne -> S.Decode $ readb n ne.spine $ readb n ne.head
+    V.InitDecode ne -> S.Decode $ readb n ne.spine $ readb n ne.name
     V.Function f -> S.Function $ readb n f
     V.Record r -> S.Record $ readb n r
     V.Eq eq -> S.Eq $ readb n eq
@@ -103,5 +107,6 @@ instance Readback V.TypeBehavior S.TypeBehavior where
     V.LikeU u -> S.LikeU u
     V.LikeRecord rt -> S.LikeRecord $ readb n rt
     V.LikeFunction ft -> S.LikeFunction $ readb n ft
+    V.LikeInductive ne -> S.LikeInductive $ readb n ne.spine $ readb n ne.name
     V.LikeBuiltinTy bt -> S.LikeBuiltinTy bt
     V.NoRules -> S.NoRules
diff --git a/packages/coln-compiler/src/Coln/Core/Syntax.hs b/packages/coln-compiler/src/Coln/Core/Syntax.hs
index e8dc774e..813ceb0b 100644
--- a/packages/coln-compiler/src/Coln/Core/Syntax.hs
+++ b/packages/coln-compiler/src/Coln/Core/Syntax.hs
@@ -23,6 +23,7 @@ data El :: Case -> Type where
   App :: El N -> El N -> El N
   Cons :: Dict (El c) -> El c
   Proj :: El N -> Name -> El N
+  Init :: Ty N -> El D
   Lit :: Literal -> El N
   Is :: El N -> El D
   Lookup :: TableName -> Dict (El N) -> Ty N -> El N
@@ -58,5 +59,6 @@ data TypeBehavior
   = LikeU Universe
   | LikeFunction (FunctionType Ty)
   | LikeRecord (RecordType Ty)
+  | LikeInductive (El N)
   | LikeBuiltinTy BuiltinTy
   | NoRules
diff --git a/packages/coln-compiler/src/Coln/Core/Value.hs b/packages/coln-compiler/src/Coln/Core/Value.hs
index 5fc0ffee..d08c76ae 100644
--- a/packages/coln-compiler/src/Coln/Core/Value.hs
+++ b/packages/coln-compiler/src/Coln/Core/Value.hs
@@ -36,6 +36,7 @@ type family Evaluation (f :: Case -> Type) (c :: Case) = r | r -> c f where
 data Description :: (Case -> Type) -> Type where
   Describe :: f D -> Description f
   Become :: f N -> Description f
+  BecomeWith :: (BareNeutral -> f N) -> Description f
 
 class HasEvaluation (c :: Case) where
   epure :: a c -> Evaluation a c
@@ -53,8 +54,10 @@ instance HasEvaluation D where
   epure = Describe
   emap f (Describe x) = Describe (f x)
   emap f (Become x) = Become (f x)
+  emap f (BecomeWith g) = BecomeWith (f . g)
   ebind f (Describe x) = f x
   ebind f (Become x) = Become (f x)
+  ebind f (BecomeWith g) = BecomeWith (f . g)
   scase = SDescriptive
 
 -- Abstractions
@@ -76,6 +79,11 @@ data Spine
   | App Spine (El N)
   | Proj Spine Name
 
+composeSpines :: Spine -> Spine -> Spine
+composeSpines s Id = s
+composeSpines s (App s' v) = App (composeSpines s s') v
+composeSpines s (Proj s' x) = Proj (composeSpines s s') x
+
 data Head
   = LocalVar FId
   | GlobalVar Name ~(El N)
@@ -120,6 +128,7 @@ reflect head spine ~ty edesc = do
   case edesc of
     Just (Describe desc) -> k (Just desc)
     Just (Become v) -> v
+    Just (BecomeWith f) -> f (BareNeutral head spine)
     Nothing -> k Nothing
 
 local :: FId -> Ty N -> El N
@@ -152,8 +161,18 @@ instance ToBare DecodedNeutral where
 -- Elements
 --------------------------------------------------------------------------------
 
+data InitNeutral = InitNeutral
+  { name :: BareNeutral
+  , initialOf :: Ty N
+  , spine :: Spine
+  }
+
+fullNeu :: InitNeutral -> BareNeutral
+fullNeu n = BareNeutral n.name.head (composeSpines n.name.spine n.spine)
+
 data El :: Case -> Type where
   Neu :: Neutral -> El N
+  InitNeu :: InitNeutral -> El N
   Code :: Ty c -> El c
   Lam :: ~(Ty N) -> Clo El c -> El c
   Cons :: Dict (Evaluation El c) -> El c
@@ -190,6 +209,11 @@ data RecordType = RecordType
   , fieldTypes :: Dict (Locals -> Ty N)
   }
 
+data InductiveType = InductiveType
+  { initialOf :: Ty N
+  , spine :: Spine
+  }
+
 data EqualityType = EqualityType
   { at :: Ty N
   , lhs :: El N
@@ -206,6 +230,7 @@ typeForProjection rt x fields = do
 data Ty :: Case -> Type where
   U :: Universe -> Ty N
   Decode :: DecodedNeutral -> Ty N
+  InitDecode :: InitNeutral -> Ty N
   Function :: FunctionType -> Ty N
   Record :: RecordType -> Ty D
   Eq :: EqualityType -> Ty N
@@ -216,6 +241,7 @@ instance DebugVal (Ty c) where
   debugVal = \case
     U _ -> "U"
     Decode _ -> "Decode"
+    InitDecode _ -> "InitDecode"
     Function _ -> "Function"
     Record _ -> "Record"
     Eq _ -> "Eq"
@@ -228,6 +254,7 @@ instance LevelOf (Ty c) where
     Decode n -> decodesInto n.universe
     Function ft -> levelOf ft.variant
     Record rt -> rt.level
+    InitDecode _ -> Level Set HSet
     Eq ety -> Level (levelOf ety.at).mlevel (equalityHLevelOf (levelOf ety.at).hlevel)
     BuiltinTy _ -> Level Set HSet -- Only Int/String so far
     EltOf _ _ -> Level Set HSet -- TODO
@@ -236,8 +263,9 @@ behavior :: Ty c -> TypeBehavior
 behavior = \case
   U u -> LikeU u
   Decode n -> case n.description of
-    Just (Record rt) -> LikeRecord rt
+    Just t -> behavior t
     Nothing -> NoRules
+  InitDecode n -> LikeInductive n
   Function ft -> LikeFunction ft
   Record rt -> LikeRecord rt
   Eq _ -> NoRules
@@ -254,7 +282,9 @@ decode (Neu n) = do
   case decode <$> n.description of
     Just (Describe desc) -> k (Just desc)
     Just (Become ty) -> ty
+    Just (BecomeWith f) -> f (BareNeutral n.head n.spine)
     Nothing -> k Nothing
+decode (InitNeu n) = InitDecode n
 decode _ = panic "ill-typed decoding"
 
 -- Type behavior
@@ -264,6 +294,7 @@ data TypeBehavior
   = LikeU Universe
   | LikeFunction FunctionType
   | LikeRecord RecordType
+  | LikeInductive InitNeutral
   | LikeBuiltinTy BuiltinTy
   | NoRules
 
@@ -272,6 +303,7 @@ instance DebugVal TypeBehavior where
     LikeU _ -> "LikeU"
     LikeFunction _ -> "LikeFunction"
     LikeRecord _ -> "LikeRecord"
+    LikeInductive _ -> "LikeInductive"
     LikeBuiltinTy _ -> "LikeBuiltinTy"
     NoRules -> "NoRules"
 
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Coercion.hs b/packages/coln-compiler/src/Coln/Elaborator/Coercion.hs
new file mode 100644
index 00000000..12a74a6b
--- /dev/null
+++ b/packages/coln-compiler/src/Coln/Elaborator/Coercion.hs
@@ -0,0 +1,36 @@
+-- SPDX-FileCopyrightText: 2026 Coln contributors
+--
+-- SPDX-License-Identifier: Apache-2.0 OR MIT
+
+module Coln.Elaborator.Coercion where
+
+import Coln.Common
+import Coln.Core
+import Coln.Core.Memoed qualified as M
+import Coln.Core.Value qualified as V
+import Coln.Elaborator.Judgment
+import Coln.Elaborator.Rules.Polarity qualified as Polarity
+import Coln.Elaborator.Rules.Universe qualified as Universe
+
+intoTyp :: Span -> Judgment N -> Typ N
+intoTyp _ (FromTyp t) = t
+intoTyp sp (FromSyn s) = Universe.elimSyn sp s
+intoTyp _ (FromChk _ c) = Universe.elim TheoryU c
+
+intoSyn :: (V.HasEvaluation c) => DDoc -> Span -> Judgment c -> Syn c
+intoSyn _ sp (FromTyp t) = Syn $ \e -> do
+  raw <- t.elab e
+  case universeFor (levelOf raw) of
+    Nothing -> do
+      let msg = "type" <+> prtIn e raw <+> "too large to fit in a universe"
+      failWith e.diagEnv sp TypeTooLarge msg
+    Just u -> pure (V.U u, M.code raw)
+intoSyn _ _ (FromSyn s) = s
+intoSyn use sp (FromChk nd _) = Syn $ \e -> do
+  let msg = "Type annotation required when using a" <+> nd <+> "as" <+> use
+  failWith e.diagEnv sp AnnotationRequired msg
+
+intoChk :: (V.HasEvaluation c) => Span -> Judgment c -> Chk c
+intoChk sp (FromTyp t) = Universe.intro sp t
+intoChk sp (FromSyn s) = Polarity.conv sp s
+intoChk _ (FromChk _ c) = c
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Diagnostics.hs b/packages/coln-compiler/src/Coln/Elaborator/Diagnostics.hs
index dc47885b..7bfe9ee8 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Diagnostics.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Diagnostics.hs
@@ -29,6 +29,8 @@ data ElaboratorCode
   | MismatchedRecordField
   | VariableNotInScope
   | DebugMisc
+  | InductiveInConjunctive
+  | InitInConjunctive
   deriving (Eq, Ord)
 
 elaboratorCodeTable :: Map ElaboratorCode CodeMeta
@@ -50,4 +52,6 @@ elaboratorCodeTable =
     , (MismatchedRecordField, CodeMeta 13 SError Nothing)
     , (VariableNotInScope, CodeMeta 14 SError Nothing)
     , (DebugMisc, CodeMeta 15 SDebug Nothing)
+    , (InductiveInConjunctive, CodeMeta 16 SError Nothing)
+    , (InitInConjunctive, CodeMeta 17 SError Nothing)
     ]
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Environment.hs b/packages/coln-compiler/src/Coln/Elaborator/Environment.hs
index 2f5508ce..5f94e5a8 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Environment.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Environment.hs
@@ -5,7 +5,7 @@
 module Coln.Elaborator.Environment where
 
 import Coln.Common
-import Coln.Core
+import Coln.Core hiding (GlobalEntry (..))
 import Coln.Core.Value qualified as BN (BareNeutral (..))
 import Coln.Core.Value qualified as V
 import Coln.Elaborator.Diagnostics
@@ -17,48 +17,57 @@ data Scope = Scope
   { len :: Int
   , names :: Bwd Name
   , locals :: V.Locals
-  , ctx :: Bwd (V.Ty N)
+  , ctx :: Bwd (V.Ty N, Mode)
+  , mode :: Mode
   }
 
-emptyScope :: Scope
+lock :: Scope -> Scope
+lock sc = sc{mode = Conjunctive, ctx = fmap (\(a, _) -> (a, Inductive)) sc.ctx}
+
+unlock :: Scope -> Scope
+unlock sc = sc{mode = Inductive}
+
+emptyScope :: Mode -> Scope
 emptyScope = Scope 0 BwdNil V.LNil BwdNil
 
 instance HasShape Scope where
   shape :: Scope -> CtxShape
   shape c = CtxShape c.len c.names
 
-bind :: Name -> V.Ty N -> Scope -> Scope
-bind x a c = do
+bind :: Name -> V.Ty N -> Mode -> Scope -> Scope
+bind x a m c = do
   let v = V.local (FId c.len) a
-  let_ x v a c
+  let_ x v a m c
 
-let_ :: Name -> V.El N -> V.Ty N -> Scope -> Scope
-let_ x v a c =
+let_ :: Name -> V.El N -> V.Ty N -> Mode -> Scope -> Scope
+let_ x v a m c =
   Scope
     (c.len + 1)
     (c.names :> x)
     (V.LSnoc c.locals v)
-    (c.ctx :> a)
+    (c.ctx :> (a, m))
+    c.mode
 
-withBound :: Name -> V.Ty N -> Scope -> (V.El N -> Scope -> a) -> a
-withBound x a c body = do
+withBound :: Name -> V.Ty N -> Mode -> Scope -> (V.El N -> Scope -> a) -> a
+withBound x a m c body = do
   let v = V.local (FId c.len) a
-  let c' = let_ x v a c
+  let c' = let_ x v a m c
   body v c'
 
-instance Lookup Scope Name (BId, V.El N, V.Ty N) where
+instance Lookup Scope Name (BId, V.El N, V.Ty N, Mode) where
   lookup sc x = go sc.len sc.len sc.names sc.locals sc.ctx 0
    where
+    go :: Int -> Int -> Bwd Name -> V.Locals -> Bwd (V.Ty N, Mode) -> Int -> Maybe (BId, V.El N, V.Ty N, Mode)
     go 0 0 BwdNil V.LNil BwdNil _ = Nothing
     go 0 0 BwdNil (V.LSnocChunk vs chunk) BwdNil i
       | Vector.length chunk == 0 = go 0 0 BwdNil vs BwdNil i
-    go n _ (xs :> x') (V.LSnoc vs v) (ts :> t) i
-      | x' == x = Just (BId i, v, t)
+    go n _ (xs :> x') (V.LSnoc vs v) (ts :> (t, m)) i
+      | x' == x = Just (BId i, v, t, m)
       | otherwise = go (n - 1) (n - 1) xs vs ts (i + 1)
-    go n m xs@(xs' :> x') vs@(V.LSnocChunk vs' chunk) ts@(ts' :> t) i
-      | m - n == Vector.length chunk = go n n xs vs' ts i
-      | x' == x = Just (BId i, chunk Vector.! (Vector.length chunk + n - m - 1), t)
-      | otherwise = go n m xs' vs ts' (i + 1)
+    go n n' xs@(xs' :> x') vs@(V.LSnocChunk vs' chunk) ts@(ts' :> (t, m)) i
+      | n' - n == Vector.length chunk = go n n xs vs' ts i
+      | x' == x = Just (BId i, chunk Vector.! (Vector.length chunk + n - n' - 1), t, m)
+      | otherwise = go n n' xs' vs ts' (i + 1)
     go _ _ _ _ _ _ = panic "misaligned local variable details"
 
 -- * Target
@@ -91,21 +100,21 @@ data ElabEnv c = ElabEnv
 instance HasShape (ElabEnv c) where
   shape e = shape e.scope
 
-emptyElabEnvFor :: DiagnosticEnv ElaboratorCode -> Globals -> Name -> V.Ty N -> ElabEnv D
-emptyElabEnvFor diagEnv globals x ty = do
+emptyElabEnvFor :: DiagnosticEnv ElaboratorCode -> Globals -> Mode -> Name -> V.Ty N -> ElabEnv D
+emptyElabEnvFor diagEnv globals m x ty = do
   let v = V.reflect (V.GlobalVar x v) V.Id ty Nothing
   ElabEnv
     { target = (TargetNamed (V.BareNeutral (V.GlobalVar x v) V.Id))
-    , scope = emptyScope
+    , scope = emptyScope m
     , globals = globals
     , diagEnv = diagEnv
     }
 
-emptyElabEnv :: DiagnosticEnv ElaboratorCode -> Globals -> ElabEnv N
-emptyElabEnv diagEnv globals =
+emptyElabEnv :: DiagnosticEnv ElaboratorCode -> Globals -> Mode -> ElabEnv N
+emptyElabEnv diagEnv globals m =
   ElabEnv
     { target = TargetAnonymous
-    , scope = emptyScope
+    , scope = emptyScope m
     , globals = globals
     , diagEnv = diagEnv
     }
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Judgment.hs b/packages/coln-compiler/src/Coln/Elaborator/Judgment.hs
index d6473c5d..ceb58a42 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Judgment.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Judgment.hs
@@ -11,10 +11,6 @@ module Coln.Elaborator.Judgment (
   Chk (..),
   Judgment (..),
   useIs,
-  intoTyp,
-  intoSyn,
-  intoChk,
-  annotate,
 )
 where
 
@@ -43,55 +39,6 @@ useIs @c f e = fmap change $ f e{target = TargetAnonymous}
     SNominative -> id
     SDescriptive -> M.is
 
-intoTyp :: Span -> Judgment N -> Typ N
-intoTyp _ (FromTyp t) = t
-intoTyp sp (FromSyn s) = Typ $ \e -> do
-  (ty, el) <- s.elab e
-  case V.behavior ty of
-    V.LikeU _ -> pure $ M.decode el
-    _ -> do
-      let msg = "tried to use a value of type" <+> prtIn e ty <+> "as a type"
-      failWith e.diagEnv sp TypeMismatch msg
-intoTyp _ (FromChk _ c) = Typ $ \e -> do
-  el <- c.elab e $ V.U TheoryU
-  pure $ M.decode el
-
-intoSyn :: (V.HasEvaluation c) => DDoc -> Span -> Judgment c -> Syn c
-intoSyn _ sp (FromTyp t) = Syn $ \e -> do
-  raw <- t.elab e
-  case universeFor (levelOf raw) of
-    Nothing -> do
-      let msg = "type" <+> prtIn e raw <+> "too large to fit in a universe"
-      failWith e.diagEnv sp TypeTooLarge msg
-    Just u -> pure (V.U u, M.code raw)
-intoSyn _ _ (FromSyn s) = s
-intoSyn use sp (FromChk nd _) = Syn $ \e -> do
-  let msg = "Type annotation required when using a" <+> nd <+> "as" <+> use
-  failWith e.diagEnv sp AnnotationRequired msg
-
-intoChk :: (V.HasEvaluation c) => Span -> Judgment c -> Chk c
-intoChk sp (FromTyp t) = Chk $ \e ty -> do
-  raw <- t.elab e
-  case V.behavior ty of
-    V.LikeU u -> do
-      case leq (levelOf raw) (decodesInto u) of
-        True -> pure $ M.code raw
-        False -> do
-          let msg = "type" <+> prtIn e raw <+> "too large for universe" <+> pretty u
-          failWith e.diagEnv sp TypeTooLarge msg
-    _ -> do
-      let msg = "cannot check type" <+> prtIn e raw <+> "at non-universe type" <+> prtIn e.scope ty
-      failWith e.diagEnv sp TypeAtNonUniverse msg
-intoChk sp (FromSyn s) = Chk $ \e ty -> do
-  (ty', el) <- s.elab e
-  case defEq (shape e) ty ty' of
-    Right _ -> pure el
-    Left err -> do
-      let msg = "expected type" <+> prtIn e.scope ty <> ", but got type" <+> prtIn e.scope ty'
-      let note = Just $ dpretty err
-      failWithNote e.diagEnv sp TypeMismatch msg note
-intoChk _ (FromChk _ c) = c
-
 annotate :: Typ N -> Chk c -> Syn c
 annotate t c = Syn \e -> do
   a <- t.elab (e{target = TargetAnonymous})
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
index 16945f76..ca3ed349 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
@@ -10,33 +10,37 @@ import Coln.Core.Syntax qualified as S
 import Coln.Core.Value qualified as V
 import Coln.Elaborator.Judgment
 
-variantFor :: Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
-variantFor dom cod sp e =
+variantFor :: Mode -> Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
+variantFor m dom cod sp e =
   case functionMLevelFor (levelOf dom).mlevel (levelOf cod).mlevel of
-    Just l -> pure (FunctionVariant l (levelOf cod).hlevel)
+    Just l -> pure (FunctionVariant l (levelOf cod).hlevel m)
     Nothing -> do
       let msg = "higher-order theories are not supported"
       failWith e.diagEnv sp FunctionDomainTooLarge msg
 
-data Binder = Anonymous (Typ N) | Named Name (Typ N)
+data Binder = Anonymous Mode (Typ N) | Named Mode Name (Typ N)
+
+shiftToMode :: Mode -> Scope -> Scope
+shiftToMode Conjunctive sc = sc
+shiftToMode Inductive sc = unlock sc
 
 formation :: Span -> Binder -> Typ N -> Typ N
-formation sp (Anonymous dom) cod = Typ \e -> do
-  edom <- dom.elab e
+formation sp (Anonymous m dom) cod = Typ \e -> do
+  edom <- dom.elab (e{scope = shiftToMode m e.scope})
   ecod <- cod.elab e
-  v <- variantFor edom ecod sp e
+  v <- variantFor m edom ecod sp e
   pure $ function e.scope.locals v edom (S.AbsConst ecod)
-formation sp (Named x dom) cod = Typ \e -> do
-  edom <- dom.elab e
-  ecod <- cod.elab $ e{scope = bind x edom.val e.scope}
-  v <- variantFor edom ecod sp e
+formation sp (Named m x dom) cod = Typ \e -> do
+  edom <- dom.elab (e{scope = shiftToMode m e.scope})
+  ecod <- cod.elab $ e{scope = bind x edom.val m e.scope}
+  v <- variantFor m edom ecod sp e
   pure $ function e.scope.locals v edom (S.Abs x ecod)
 
 intro :: (V.HasEvaluation c) => Span -> Name -> Chk c -> Chk c
 intro sp x body = Chk \e a ->
   case V.behavior a of
     V.LikeFunction ft -> do
-      ebody <- withBound x ft.dom e.scope $ \v scope' ->
+      ebody <- withBound x ft.dom ft.variant.domainMode e.scope $ \v scope' ->
         body.elab
           (e{scope = scope', target = appTarget e.target v})
           (V.appClo ft.cod v)
@@ -50,7 +54,7 @@ elim sp callee arg = Syn $ \e -> do
   (ty, ecallee) <- callee.elab e
   case V.behavior ty of
     V.LikeFunction ft -> do
-      earg <- arg.elab e ft.dom
+      earg <- arg.elab (e{scope = shiftToMode ft.variant.domainMode e.scope}) ft.dom
       pure (V.appClo ft.cod earg.val, app ecallee earg)
     _ -> do
       let msg = "tried to apply a value that was not of a function type"
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Initial.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Initial.hs
new file mode 100644
index 00000000..b2fc2919
--- /dev/null
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Initial.hs
@@ -0,0 +1,22 @@
+-- SPDX-FileCopyrightText: 2026 Coln contributors
+--
+-- SPDX-License-Identifier: Apache-2.0 OR MIT
+
+module Coln.Elaborator.Rules.Initial where
+
+import Prelude hiding (init)
+
+import Coln.Common
+import Coln.Core
+import Coln.Elaborator.Environment
+import Coln.Elaborator.Judgment
+
+create :: Span -> Typ N -> Syn D
+create sp t = Syn \e -> do
+  case e.scope.mode of
+    Inductive -> pure ()
+    Conjunctive -> do
+      let msg = "cannot create initial model in conjunctive mode"
+      failWith e.diagEnv sp InitInConjunctive msg
+  a <- t.elab (e{scope = lock e.scope, target = TargetAnonymous})
+  pure (a.val, init a)
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Polarity.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Polarity.hs
new file mode 100644
index 00000000..8ee54055
--- /dev/null
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Polarity.hs
@@ -0,0 +1,26 @@
+-- SPDX-FileCopyrightText: 2026 Coln contributors
+--
+-- SPDX-License-Identifier: Apache-2.0 OR MIT
+
+module Coln.Elaborator.Rules.Polarity where
+
+import Coln.Common
+import Coln.Core
+import Coln.Core.Value qualified as V
+import Coln.Elaborator.Judgment
+
+conv :: (V.HasEvaluation c) => Span -> Syn c -> Chk c
+conv sp s = Chk \e a -> do
+  (a', m) <- s.elab e
+  case defEq (shape e) a a' of
+    Right _ -> pure m
+    Left err -> do
+      let msg = "expected type" <+> prtIn e.scope a <> ", but got type" <+> prtIn e.scope a'
+      let note = Just $ dpretty err
+      failWithNote e.diagEnv sp TypeMismatch msg note
+
+annot :: (V.HasEvaluation c) => Chk c -> Typ N -> Syn c
+annot c t = Syn \e -> do
+  a <- t.elab (e{target = TargetAnonymous})
+  m <- c.elab e a.val
+  pure (a.val, m)
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
index c0af41ba..b51501b8 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
@@ -22,7 +22,7 @@ formation fieldTyps = Typ $ \e -> do
   let go _ [] = pure (Level Set HUnit, [])
       go e' ((FieldDeclaration x typ) : rest) = do
         ty <- typ.elab e'
-        (l, fieldTys) <- go (e'{scope = bind x ty.val e'.scope}) rest
+        (l, fieldTys) <- go (e'{scope = bind x ty.val Conjunctive e'.scope}) rest
         pure (maxLevel l (levelOf ty), (x, ty) : fieldTys)
       go e' ((FieldDeclarationDebug ds) : rest) = do
         runDebug e' ds
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Universe.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Universe.hs
index 2c3ecc46..37d02cf9 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Universe.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Universe.hs
@@ -4,8 +4,38 @@
 
 module Coln.Elaborator.Rules.Universe where
 
+import Coln.Common
 import Coln.Core
+import Coln.Core.Value qualified as V
 import Coln.Elaborator.Judgment
 
 formation :: Universe -> Typ N
 formation u = Typ \_ -> pure $ univ u
+
+intro :: (V.HasEvaluation c) => Span -> Typ c -> Chk c
+intro sp t = Chk $ \e ty -> do
+  raw <- t.elab e
+  case V.behavior ty of
+    V.LikeU u -> do
+      case leq (levelOf raw) (decodesInto u) of
+        True -> pure $ code raw
+        False -> do
+          let msg = "type" <+> prtIn e raw <+> "too large for universe" <+> pretty u
+          failWith e.diagEnv sp TypeTooLarge msg
+    _ -> do
+      let msg = "cannot check type" <+> prtIn e raw <+> "at non-universe type" <+> prtIn e.scope ty
+      failWith e.diagEnv sp TypeAtNonUniverse msg
+
+elim :: Universe -> Chk N -> Typ N
+elim u c = Typ \e -> do
+  el <- c.elab e $ V.U u
+  pure $ decode el
+
+elimSyn :: Span -> Syn N -> Typ N
+elimSyn sp s = Typ \e -> do
+  (a, el) <- s.elab e
+  case V.behavior a of
+    V.LikeU _ -> pure $ decode el
+    _ -> do
+      let msg = "expected element of universe type"
+      failWith e.diagEnv sp TypeAtNonUniverse msg
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Variable.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Variable.hs
index 300e1fd5..c287beab 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Variable.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Variable.hs
@@ -14,11 +14,16 @@ import Coln.Elaborator.Environment
 import Coln.Elaborator.Judgment
 
 find :: Span -> Name -> Syn N
-find sp x = Syn \e ->
-  case lookup e.scope x of
-    Just (i, v, ty) -> pure (ty, localVar i v)
+find sp x = Syn \e -> do
+  (ty, tm, m) <- case lookup e.scope x of
+    Just (i, v, ty, m) -> pure (ty, localVar i v, m)
     Nothing -> case lookup e.globals x of
-      Just ge -> pure (ge.ty, globalVar x ge.val)
+      Just ge -> pure (ge.ty, globalVar x ge.val, ge.mode)
       Nothing -> do
         let msg = "no such variable" <+> dpretty x <+> "in scope"
         failWith e.diagEnv sp VariableNotInScope msg
+  case (m, e.scope.mode) of
+    (Inductive, Conjunctive) -> do
+      let msg = "cannot use inductively bound variable in a conjunctive context"
+      failWith e.diagEnv sp InductiveInConjunctive msg
+    _ -> pure (ty, tm)
diff --git a/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs b/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
index 095e484b..7f37db5f 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Diagnostics.hs
@@ -14,6 +14,8 @@ data ParserCode
   | UnexpectedField
   | UnexpectedDescriptive
   | UnknownCommand
+  | UnknownModifiers
+  | UnknownMode
   deriving (Eq, Ord)
 
 parserCodeTable :: Map ParserCode CodeMeta
@@ -25,4 +27,6 @@ parserCodeTable =
     , (UnexpectedField, CodeMeta 3 SError Nothing)
     , (UnexpectedDescriptive, CodeMeta 4 SError Nothing)
     , (UnknownCommand, CodeMeta 5 SError Nothing)
+    , (UnknownModifiers, CodeMeta 6 SError Nothing)
+    , (UnknownMode, CodeMeta 7 SError Nothing)
     ]
diff --git a/packages/coln-compiler/src/Coln/Frontend/Notation.hs b/packages/coln-compiler/src/Coln/Frontend/Notation.hs
index 86a9b646..41d9d6d8 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Notation.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Notation.hs
@@ -22,6 +22,7 @@ lexConfig =
     , ("showtype", K.Decl)
     , ("showlevel", K.Decl)
     , ("expand", K.Decl)
+    , ("ind", K.Modifier)
     , ("end", K.End)
     , ("Set", K.AKeyword)
     , ("Prop", K.AKeyword)
diff --git a/packages/coln-compiler/src/Coln/Frontend/Parser.hs b/packages/coln-compiler/src/Coln/Frontend/Parser.hs
index 7fe780c5..21ef6a68 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Parser.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Parser.hs
@@ -1,243 +1,11 @@
 -- SPDX-FileCopyrightText: 2026 Coln contributors
 --
 -- SPDX-License-Identifier: Apache-2.0 OR MIT
-{-# LANGUAGE TypeAbstractions #-}
 
-module Coln.Frontend.Parser where
+module Coln.Frontend.Parser (
+  module Coln.Frontend.Parser.Expr,
+  module Coln.Frontend.Parser.Top,
+) where
 
-import Control.Exception (try)
-import Data.Foldable
-import Data.Functor.Contravariant (contramap)
-import Data.List.NonEmpty (NonEmpty (..))
-import FNotation (Ntn)
-import FNotation qualified as N
-
-import Coln.Common
-import Coln.Core
-import Coln.Core.Layout
-import Coln.Core.Memoed qualified as M
-import Coln.Core.Value qualified as V
-import Coln.Diagnostics
-import Coln.Elaborator.Debug
-import Coln.Elaborator.Environment
-import Coln.Elaborator.Judgment
-import Coln.Elaborator.Rules.Builtin qualified as Builtin
-import Coln.Elaborator.Rules.Equality qualified as Equality
-import Coln.Elaborator.Rules.Function qualified as Function
-import Coln.Elaborator.Rules.Record qualified as Record
-import Coln.Elaborator.Rules.Universe qualified as Universe
-import Coln.Elaborator.Rules.Variable qualified as Variable
-import Coln.Frontend.Diagnostics
-import Coln.Frontend.Notation
-
-type ParseEnv = DiagnosticEnv ColnCode
-
-top :: ParseEnv -> [Ntn] -> IO Globals
-top e = foldlM (decl' e) emptyGlobals
-
-topFromText :: Reporter ColnCode -> File -> IO Globals
-topFromText r f = do
-  ts <- N.lex lexConfig (contramap LexerCode r) f
-  ns <- N.read readConfig (contramap ReaderCode r) f ts
-  top (DiagnosticEnv r f) ns
-
-decl' :: ParseEnv -> Globals -> Ntn -> IO Globals
-decl' e g n = do
-  try (decl e g n) >>= \case
-    Right g' -> pure g'
-    Left (_ :: FailException) -> pure g
-
-decl :: ParseEnv -> Globals -> Ntn -> IO Globals
-decl e g (N.Decl "theory" n _) = do
-  (x, ge) <- idef e g (M.univ TheoryU) n
-  pure $ addGlobalEntry x ge g
-decl e g (N.Decl "def" n _) = do
-  (x, ge) <- def e g n
-  pure $ addGlobalEntry x ge g
-decl e g (N.Block "realm" (Just head) body _) = do
-  (x, r) <- realm e g head body
-  pure $ addRealm x r g
-decl e _ n = unexpectedNotation e n "top-level declaration"
-
-definition :: ParseEnv -> Ntn -> IO (Ntn, Ntn)
-definition _ (N.Infix n0 (N.Keyword ":=" _) n1) = pure (n0, n1)
-definition e n = unexpectedNotation e n "notation of the form `<head> := <body>`"
-
-annot :: ParseEnv -> Ntn -> IO (Ntn, Ntn)
-annot _ (N.Infix n0 (N.Keyword ":" _) n1) = pure (n0, n1)
-annot e n = unexpectedNotation e n "type-annotated expression, e.g. `<pattern> : <type>`"
-
-debugCommand :: ParseEnv -> Span -> Name -> Ntn -> IO DebugCommand
-debugCommand e _ "showtype" n = do
-  s <- syn e "argument to showtype" n
-  pure $ ShowType (N.span n) s
-debugCommand e _ "showtypeb" n = do
-  s <- syn e "argument to showtypeb" n
-  pure $ ShowTypeBehavior (N.span n) s
-debugCommand e _ "showlevel" n = do
-  ty <- typ e n
-  pure $ ShowLevel (N.span n) ty
-debugCommand e _ "expand" n = do
-  s <- syn e "argument to expand" n
-  pure $ Expand (N.span n) s
-debugCommand e sp x _ = unknownCommand e sp x
-
-fieldDecl :: ParseEnv -> Ntn -> IO Record.FieldDeclaration
-fieldDecl e (N.Infix (N.Ident x _) (N.Keyword ":" _) n) =
-  Record.FieldDeclaration x <$> typ e n
-fieldDecl e (N.Decl c n sp) =
-  Record.FieldDeclarationDebug <$> debugCommand e sp c n
-fieldDecl e n = unexpectedNotation e n "field declaration of the form `<fieldname> : <type>`"
-
-fieldSetting :: (V.HasEvaluation c) => ParseEnv -> Ntn -> IO (Record.FieldSetting c)
-fieldSetting e (N.Infix (N.Ident x sp) (N.Keyword ":=" _) body) =
-  Record.FieldSetting x <$> chk e body <*> pure sp
-fieldSetting e n = unexpectedNotation e n "field setting of the form `<fieldname> := <expr>`"
-
-ident :: ParseEnv -> Ntn -> IO Name
-ident _ (N.Ident x _) = pure x
-ident e n = unexpectedNotation e n "identifier"
-
-argBinding :: ParseEnv -> Ntn -> IO (Span, Name, Ntn)
-argBinding e n@(N.Infix n0 (N.Keyword ":" _) n1) = do
-  x <- ident e n0
-  pure (N.span n, x, n1)
-argBinding e n = unexpectedNotation e n "argument binding of the form `<name> : <type>`"
-
-unpackArgs :: ParseEnv -> Ntn -> IO (Name, [(Span, Name, Ntn)])
-unpackArgs e (N.Group (xN :| argsN)) = do
-  x <- ident e xN
-  args <- mapM (argBinding e) argsN
-  pure (x, args)
-
-def :: ParseEnv -> Globals -> Ntn -> IO (Name, GlobalEntry)
-def e g n = do
-  (head_n, body_n) <- definition e n
-  (pat_n, ty_n) <- annot e head_n
-  (name, args) <- unpackArgs e pat_n
-  ret_typ <- typ e ty_n
-  body_chk <- chk e body_n
-  (ty_j, term_j) <- withArgs e args (ret_typ, body_chk)
-  let tyElabE = emptyElabEnv (contramap ElaboratorCode e) g
-  ty <- ty_j.elab tyElabE
-  let elabE = emptyElabEnvFor (contramap ElaboratorCode e) g name ty.val
-  term <- term_j.elab elabE ty.val
-  let entry = M.mkGlobal name ty.val term
-  pure (name, entry)
-
-idef :: ParseEnv -> Globals -> M.Ty N -> Ntn -> IO (Name, GlobalEntry)
-idef e g ret_ty n = do
-  (pat_n, body_n) <- definition e n
-  (name, args) <- unpackArgs e pat_n
-  body_chk <- chk e body_n
-  (ty_j, term_j) <- withArgs e args $ (Typ \_ -> pure ret_ty, body_chk)
-  let tyElabE = emptyElabEnv (contramap ElaboratorCode e) g
-  ty <- ty_j.elab tyElabE
-  let elabE = emptyElabEnvFor (contramap ElaboratorCode e) g name ty.val
-  term <- term_j.elab elabE ty.val
-  let entry = M.mkGlobal name ty.val term
-  pure (name, entry)
-
-realmHead :: ParseEnv -> Ntn -> IO (Name, Ntn)
-realmHead _ (N.Infix (N.Ident x _) (N.Keyword "@" _) n) = pure (x, n)
-realmHead e n = unexpectedNotation e n "realm head"
-
-realm :: ParseEnv -> Globals -> Ntn -> [Ntn] -> IO (Name, Realm)
-realm e g head _defs = do
-  (x, theory_n) <- realmHead e head
-  theory_typ <- typ e theory_n
-  theory <- theory_typ.elab (emptyElabEnv (contramap ElaboratorCode e) g)
-  let (gt, root) = layoutTop x theory.val
-  pure (x, Realm gt root.val theory.val)
-
-withArgs :: (V.HasEvaluation c) => ParseEnv -> [(Span, Name, Ntn)] -> (Typ N, Chk c) -> IO (Typ N, Chk c)
-withArgs e args base = foldrM go base args
- where
-  go :: (V.HasEvaluation c) => (Span, Name, Ntn) -> (Typ N, Chk c) -> IO (Typ N, Chk c)
-  go (sp, name, n) (t, c) = do
-    argtyp <- typ e n
-    pure $
-      ( Function.formation sp (Function.Named name argtyp) t
-      , Function.intro sp name c
-      )
-
-fromSynN :: (V.HasEvaluation c) => Syn N -> Judgment c
-fromSynN @c s = case V.scase @c of
-  SNominative -> FromSyn s
-  SDescriptive -> FromSyn $ Syn \e -> do
-    (a, m) <- s.elab (e{target = TargetAnonymous})
-    pure (a, M.is m)
-
-fromTypN :: (V.HasEvaluation c) => Typ N -> Judgment c
-fromTypN @c t = case V.scase @c of
-  SNominative -> FromTyp t
-  SDescriptive -> FromTyp $ Typ \e -> do
-    m <- t.elab (e{target = TargetAnonymous})
-    pure $ M.isTy m
-
-fromTypD :: (V.HasEvaluation c) => ParseEnv -> Span -> Typ D -> IO (Judgment c)
-fromTypD @c e sp t = case V.scase @c of
-  SNominative -> do
-    let msg = "expected nominative type, got descriptive type"
-    failWith e sp (ParserCode UnexpectedDescriptive) msg
-  SDescriptive -> pure $ FromTyp t
-
-expr :: (V.HasEvaluation c) => ParseEnv -> Ntn -> IO (Judgment c)
-expr e n = case n of
-  N.Ident name s -> pure $ fromSynN $ Variable.find s name
-  N.Juxt n0 n1 -> do
-    s <- syn e "target of elimination" n0
-    fromSynN <$> elim e s n1
-  N.Keyword "Set" _ -> pure $ fromTypN $ Universe.formation SetU
-  N.Keyword "Prop" _ -> pure $ fromTypN $ Universe.formation PropU
-  N.Keyword "Int" _ -> pure $ fromTypN $ Builtin.formation BuiltinInt
-  N.Keyword "String" _ -> pure $ fromTypN $ Builtin.formation BuiltinString
-  N.Infix arg n@(N.Keyword "->" _) body ->
-    fromTypN <$> (Function.formation (N.span n) <$> binder e arg <*> typ e body)
-  N.Infix arg n@(N.Keyword "=>" _) body ->
-    FromChk "lambda expression"
-      <$> (Function.intro (N.span n) <$> ident e arg <*> chk e body)
-  n@(N.Infix lhs (N.Keyword "=" _) rhs) ->
-    fromTypN
-      <$> ( Equality.formation (N.span n)
-              <$> syn e "term in equality" lhs
-              <*> syn e "term in equality" rhs
-          )
-  N.Block "sig" Nothing ns _ -> do
-    t <- Record.formation <$> traverse (fieldDecl e) ns
-    fromTypD e (N.span n) t
-  N.Block "struct" Nothing ns s ->
-    FromChk "struct expression" <$> (Record.intro s <$> traverse (fieldSetting e) ns)
-  N.Int i _ -> pure $ fromSynN $ Builtin.intro $ LitInt i
-  N.String s _ -> pure $ fromSynN $ Builtin.intro $ LitString s
-  n -> unexpectedNotation e n "expression"
-
-syn :: (V.HasEvaluation c) => ParseEnv -> DDoc -> Ntn -> IO (Syn c)
-syn e use n = intoSyn use (N.span n) <$> expr e n
-
-chk :: (V.HasEvaluation c) => ParseEnv -> Ntn -> IO (Chk c)
-chk e n = intoChk (N.span n) <$> expr e n
-
-typ :: ParseEnv -> Ntn -> IO (Typ N)
-typ e n = intoTyp (N.span n) <$> expr e n
-
-elim :: ParseEnv -> Syn N -> Ntn -> IO (Syn N)
-elim e j = \case
-  N.Field x s -> pure $ Record.elim s j x
-  arg -> Function.elim (N.span arg) j <$> chk e arg
-
-binder :: ParseEnv -> Ntn -> IO Function.Binder
-binder e = \case
-  N.Infix name (N.Keyword ":" _) arg ->
-    Function.Named <$> ident e name <*> typ e arg
-  n -> Function.Anonymous <$> typ e n
-
-unexpectedNotation :: ParseEnv -> Ntn -> DDoc -> IO a
-unexpectedNotation e n c = do
-  let msg = "unexpected notation for" <+> c <> ":" <+> N.head n
-  failWith e (N.span n) (ParserCode UnexpectedNotation) msg
-
-unknownCommand :: ParseEnv -> Span -> Name -> IO a
-unknownCommand e sp x = do
-  let msg = "unknown command:" <+> dpretty x
-  failWith e sp (ParserCode UnknownCommand) msg
+import Coln.Frontend.Parser.Expr
+import Coln.Frontend.Parser.Top
diff --git a/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs b/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs
new file mode 100644
index 00000000..2b094e40
--- /dev/null
+++ b/packages/coln-compiler/src/Coln/Frontend/Parser/Expr.hs
@@ -0,0 +1,160 @@
+-- SPDX-FileCopyrightText: 2026 Coln contributors
+--
+-- SPDX-License-Identifier: Apache-2.0 OR MIT
+{-# LANGUAGE TypeAbstractions #-}
+
+module Coln.Frontend.Parser.Expr where
+
+import FNotation (Ntn)
+import FNotation qualified as N
+
+import Coln.Common
+import Coln.Core
+import Coln.Core.Memoed qualified as M
+import Coln.Core.Value qualified as V
+import Coln.Elaborator.Coercion
+import Coln.Elaborator.Debug
+import Coln.Elaborator.Environment
+import Coln.Elaborator.Judgment
+import Coln.Elaborator.Rules.Builtin qualified as Builtin
+import Coln.Elaborator.Rules.Equality qualified as Equality
+import Coln.Elaborator.Rules.Function qualified as Function
+import Coln.Elaborator.Rules.Initial qualified as Initial
+import Coln.Elaborator.Rules.Record qualified as Record
+import Coln.Elaborator.Rules.Universe qualified as Universe
+import Coln.Elaborator.Rules.Variable qualified as Variable
+
+import Coln.Frontend.Diagnostics
+
+type ParserEnv = DiagnosticEnv ParserCode
+
+debugCommand :: ParserEnv -> Span -> Name -> Ntn -> IO DebugCommand
+debugCommand e _ "showtype" n = do
+  s <- syn e "argument to showtype" n
+  pure $ ShowType (N.span n) s
+debugCommand e _ "showtypeb" n = do
+  s <- syn e "argument to showtypeb" n
+  pure $ ShowTypeBehavior (N.span n) s
+debugCommand e _ "showlevel" n = do
+  ty <- typ e n
+  pure $ ShowLevel (N.span n) ty
+debugCommand e _ "expand" n = do
+  s <- syn e "argument to expand" n
+  pure $ Expand (N.span n) s
+debugCommand e sp x _ = unknownCommand e sp x
+
+binder :: ParserEnv -> Ntn -> IO Function.Binder
+binder e = \case
+  N.Infix name (N.Keyword ":" _) arg -> do
+    (mode, x) <- modalIdent e Inductive name
+    Function.Named mode x <$> typ e arg
+  n -> Function.Anonymous Inductive <$> typ e n
+
+fieldDecl :: ParserEnv -> Ntn -> IO Record.FieldDeclaration
+fieldDecl e (N.Infix (N.Ident x _) (N.Keyword ":" _) n) =
+  Record.FieldDeclaration x <$> typ e n
+fieldDecl e (N.Decl c n sp) =
+  Record.FieldDeclarationDebug <$> debugCommand e sp c n
+fieldDecl e n = unexpectedNotation e n "field declaration of the form `<fieldname> : <type>`"
+
+fieldSetting :: (V.HasEvaluation c) => ParserEnv -> Ntn -> IO (Record.FieldSetting c)
+fieldSetting e (N.Infix (N.Ident x sp) (N.Keyword ":=" _) body) =
+  Record.FieldSetting x <$> chk e body <*> pure sp
+fieldSetting e n = unexpectedNotation e n "field setting of the form `<fieldname> := <expr>`"
+
+ident :: ParserEnv -> Ntn -> IO Name
+ident _ (N.Ident x _) = pure x
+ident e n = unexpectedNotation e n "identifier"
+
+modalIdent :: ParserEnv -> Mode -> Ntn -> IO (Mode, Name)
+modalIdent _ def (N.Ident x _) = pure (def, x)
+modalIdent _ _ (N.Juxt (N.Mode "i" _) (N.Ident x _)) = pure (Inductive, x)
+modalIdent _ _ (N.Juxt (N.Mode "c" _) (N.Ident x _)) = pure (Conjunctive, x)
+modalIdent e _ (N.Juxt (N.Mode _ sp) (N.Ident _ _)) =
+  failWith e sp UnknownMode "unknown mode"
+modalIdent e _ n = unexpectedNotation e n "identifier, possibly with mode annotation"
+
+unexpectedNotation :: ParserEnv -> Ntn -> DDoc -> IO a
+unexpectedNotation e n c = do
+  let msg = "unexpected notation for" <+> c <> ":" <+> N.head n
+  failWith e (N.span n) UnexpectedNotation msg
+
+unknownCommand :: ParserEnv -> Span -> Name -> IO a
+unknownCommand e sp x = do
+  let msg = "unknown command:" <+> dpretty x
+  failWith e sp UnknownCommand msg
+
+fromSynN :: (V.HasEvaluation c) => Syn N -> Judgment c
+fromSynN @c s = case V.scase @c of
+  SNominative -> FromSyn s
+  SDescriptive -> FromSyn $ Syn \e -> do
+    (a, m) <- s.elab (e{target = TargetAnonymous})
+    pure (a, M.is m)
+
+fromSynD :: (V.HasEvaluation c) => ParserEnv -> Span -> Syn D -> IO (Judgment c)
+fromSynD @c e sp s = case V.scase @c of
+  SNominative -> do
+    let msg = "expected nominative expression, got descriptive expression"
+    failWith e sp UnexpectedDescriptive msg
+  SDescriptive -> pure $ FromSyn s
+
+fromTypN :: (V.HasEvaluation c) => Typ N -> Judgment c
+fromTypN @c t = case V.scase @c of
+  SNominative -> FromTyp t
+  SDescriptive -> FromTyp $ Typ \e -> do
+    m <- t.elab (e{target = TargetAnonymous})
+    pure $ M.isTy m
+
+fromTypD :: (V.HasEvaluation c) => ParserEnv -> Span -> Typ D -> IO (Judgment c)
+fromTypD @c e sp t = case V.scase @c of
+  SNominative -> do
+    let msg = "expected nominative type, got descriptive type"
+    failWith e sp UnexpectedDescriptive msg
+  SDescriptive -> pure $ FromTyp t
+
+expr :: (V.HasEvaluation c) => ParserEnv -> Ntn -> IO (Judgment c)
+expr e n = case n of
+  N.Ident name s -> pure $ fromSynN $ Variable.find s name
+  N.Juxt (N.Keyword "init" _) n -> do
+    t <- typ e n
+    fromSynD e (N.span n) (Initial.create (N.span n) t)
+  N.Juxt n0 n1 -> do
+    s <- syn e "target of elimination" n0
+    fromSynN <$> elim e s n1
+  N.Keyword "Set" _ -> pure $ fromTypN $ Universe.formation SetU
+  N.Keyword "Prop" _ -> pure $ fromTypN $ Universe.formation PropU
+  N.Keyword "Int" _ -> pure $ fromTypN $ Builtin.formation BuiltinInt
+  N.Keyword "String" _ -> pure $ fromTypN $ Builtin.formation BuiltinString
+  N.Infix arg n@(N.Keyword "->" _) body ->
+    fromTypN <$> (Function.formation (N.span n) <$> binder e arg <*> typ e body)
+  N.Infix arg n@(N.Keyword "=>" _) body ->
+    FromChk "lambda expression"
+      <$> (Function.intro (N.span n) <$> ident e arg <*> chk e body)
+  n@(N.Infix lhs (N.Keyword "=" _) rhs) ->
+    fromTypN
+      <$> ( Equality.formation (N.span n)
+              <$> syn e "term in equality" lhs
+              <*> syn e "term in equality" rhs
+          )
+  N.Block "sig" Nothing ns _ -> do
+    t <- Record.formation <$> traverse (fieldDecl e) ns
+    fromTypD e (N.span n) t
+  N.Block "struct" Nothing ns s ->
+    FromChk "struct expression" <$> (Record.intro s <$> traverse (fieldSetting e) ns)
+  N.Int i _ -> pure $ fromSynN $ Builtin.intro $ LitInt i
+  N.String s _ -> pure $ fromSynN $ Builtin.intro $ LitString s
+  n -> unexpectedNotation e n "expression"
+
+syn :: (V.HasEvaluation c) => ParserEnv -> DDoc -> Ntn -> IO (Syn c)
+syn e use n = intoSyn use (N.span n) <$> expr e n
+
+chk :: (V.HasEvaluation c) => ParserEnv -> Ntn -> IO (Chk c)
+chk e n = intoChk (N.span n) <$> expr e n
+
+typ :: ParserEnv -> Ntn -> IO (Typ N)
+typ e n = intoTyp (N.span n) <$> expr e n
+
+elim :: ParserEnv -> Syn N -> Ntn -> IO (Syn N)
+elim e j = \case
+  N.Field x s -> pure $ Record.elim s j x
+  arg -> Function.elim (N.span arg) j <$> chk e arg
diff --git a/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs b/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs
new file mode 100644
index 00000000..3a241bb9
--- /dev/null
+++ b/packages/coln-compiler/src/Coln/Frontend/Parser/Top.hs
@@ -0,0 +1,134 @@
+-- SPDX-FileCopyrightText: 2026 Coln contributors
+--
+-- SPDX-License-Identifier: Apache-2.0 OR MIT
+
+module Coln.Frontend.Parser.Top where
+
+import Control.Exception (try)
+import Data.Foldable
+import Data.Functor.Contravariant (contramap)
+import Data.List.NonEmpty (NonEmpty (..))
+import FNotation (Ntn)
+import FNotation qualified as N
+import Prettyprinter
+
+import Coln.Common
+import Coln.Core
+import Coln.Core.Layout
+import Coln.Core.Memoed qualified as M
+import Coln.Core.Value qualified as V
+import Coln.Diagnostics
+import Coln.Elaborator.Environment
+import Coln.Elaborator.Judgment
+import Coln.Elaborator.Rules.Function qualified as Function
+import Coln.Frontend.Diagnostics
+import Coln.Frontend.Notation
+import Coln.Frontend.Parser.Expr
+
+definition :: ParserEnv -> Ntn -> IO (Ntn, Ntn)
+definition _ (N.Infix n0 (N.Keyword ":=" _) n1) = pure (n0, n1)
+definition e n = unexpectedNotation e n "notation of the form `<head> := <body>`"
+
+annot :: ParserEnv -> Ntn -> IO (Ntn, Ntn)
+annot _ (N.Infix n0 (N.Keyword ":" _) n1) = pure (n0, n1)
+annot e n = unexpectedNotation e n "type-annotated expression, e.g. `<pattern> : <type>`"
+
+argBinding :: ParserEnv -> Ntn -> IO (Span, Mode, Name, Typ N)
+argBinding e n@(N.Infix n0 (N.Keyword ":" _) n1) = do
+  (m, x) <- modalIdent e Conjunctive n0
+  a <- typ e n1
+  pure (N.span n, m, x, a)
+argBinding e n = unexpectedNotation e n "argument binding of the form `<name> : <type>`"
+
+unpackArgs :: ParserEnv -> Ntn -> IO (Name, [(Span, Mode, Name, Typ N)])
+unpackArgs e (N.Group (xN :| argsN)) = do
+  x <- ident e xN
+  args <- mapM (argBinding e) argsN
+  pure (x, args)
+
+withArgs :: (V.HasEvaluation c) => [(Span, Mode, Name, Typ N)] -> (Typ N, Chk c) -> (Typ N, Chk c)
+withArgs args base = foldr go base args
+ where
+  go :: (V.HasEvaluation c) => (Span, Mode, Name, Typ N) -> (Typ N, Chk c) -> (Typ N, Chk c)
+  go (sp, m, name, a) (t, c) =
+    ( Function.formation sp (Function.Named m name a) t
+    , Function.intro sp name c
+    )
+
+theory :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+theory e n = do
+  (pat_n, body_n) <- definition e n
+  (name, args) <- unpackArgs e pat_n
+  body <- chk e body_n
+  let (ty, tm) = withArgs args (Typ $ \_ -> pure $ M.univ TheoryU, body)
+  pure $ (name, ty, tm)
+
+def :: ParserEnv -> Ntn -> IO (Name, Typ N, Chk D)
+def e n = do
+  (head_n, body_n) <- definition e n
+  (pat_n, ty_n) <- annot e head_n
+  (name, args) <- unpackArgs e pat_n
+  returnTyp <- typ e ty_n
+  body <- chk e body_n
+  let (ty, tm) = withArgs args (returnTyp, body)
+  pure (name, ty, tm)
+
+elabEntry :: DiagnosticEnv ElaboratorCode -> Globals -> Mode -> (Name, Typ N, Chk D) -> IO GlobalEntry
+elabEntry e g m (x, ty, tm) = do
+  let tyE = emptyElabEnv e g m
+  a <- ty.elab tyE
+  let tmE = emptyElabEnvFor e g m x a.val
+  t <- tm.elab tmE a.val
+  let v = V.reflect (V.GlobalVar x v) V.Id a.val (Just t.val)
+  let entry = GlobalEntry t.stx v a.val m
+  pure entry
+
+realmHead :: ParserEnv -> Ntn -> IO (Name, Ntn)
+realmHead _ (N.Infix (N.Ident x _) (N.Keyword "@" _) n) = pure (x, n)
+realmHead e n = unexpectedNotation e n "realm head"
+
+realm :: DiagnosticEnv ColnCode -> Globals -> Ntn -> [Ntn] -> IO (Name, Realm)
+realm e g head _defs = do
+  (x, theory_n) <- realmHead (contramap ParserCode e) head
+  theory_typ <- typ (contramap ParserCode e) theory_n
+  theory <- theory_typ.elab (emptyElabEnv (contramap ElaboratorCode e) g Inductive)
+  let (gt, root) = layoutTop x theory.val
+  pure (x, Realm gt root.val theory.val)
+
+mode :: ParserEnv -> Span -> [Name] -> IO Mode
+mode _ _ [] = pure Conjunctive
+mode _ _ ["ind"] = pure Inductive
+mode e sp ms = do
+  let msg = "unknown modifiers" <+> hsep (dpretty <$> ms)
+  failWith e sp UnknownModifiers msg
+
+decl :: DiagnosticEnv ColnCode -> Globals -> Ntn -> IO Globals
+decl e g (N.MDecl ms "theory" n sp) = do
+  m <- mode (contramap ParserCode e) sp ms
+  (x, t, c) <- theory (contramap ParserCode e) n
+  ge <- elabEntry (contramap ElaboratorCode e) g m (x, t, c)
+  pure $ addGlobalEntry x ge g
+decl e g (N.MDecl ms "def" n sp) = do
+  m <- mode (contramap ParserCode e) sp ms
+  (x, t, c) <- def (contramap ParserCode e) n
+  ge <- elabEntry (contramap ElaboratorCode e) g m (x, t, c)
+  pure $ addGlobalEntry x ge g
+decl e g (N.Block "realm" (Just head) body _) = do
+  (x, r) <- realm e g head body
+  pure $ addRealm x r g
+decl e _ n = unexpectedNotation (contramap ParserCode e) n "top-level declaration"
+
+tryDecl :: DiagnosticEnv ColnCode -> Globals -> Ntn -> IO Globals
+tryDecl e g n = do
+  try (decl e g n) >>= \case
+    Right g' -> pure g'
+    Left (_ :: FailException) -> pure g
+
+top :: DiagnosticEnv ColnCode -> [Ntn] -> IO Globals
+top e = foldlM (tryDecl e) emptyGlobals
+
+topFromText :: Reporter ColnCode -> File -> IO Globals
+topFromText r f = do
+  ts <- N.lex lexConfig (contramap LexerCode r) f
+  ns <- N.read readConfig (contramap ReaderCode r) f ts
+  top (DiagnosticEnv r f) ns
diff --git a/packages/coln-compiler/test/Main.hs b/packages/coln-compiler/test/Main.hs
index 713dc5f3..db88e930 100644
--- a/packages/coln-compiler/test/Main.hs
+++ b/packages/coln-compiler/test/Main.hs
@@ -49,9 +49,10 @@ render :: DDoc -> LBS.ByteString
 render = TLE.encodeUtf8 . renderLazy . layoutPretty defaultLayoutOptions
 
 prettyEntry :: (Name, GlobalEntry) -> DDoc
-prettyEntry (x, (GlobalEntry t _ a)) =
+prettyEntry (x, (GlobalEntry t _ a m)) =
   vsep
     [ "global entry named" <+> dpretty x
+    , "in mode:" <+> dpretty m
     , "type:" <+> prtIn (CtxShape 0 BwdNil) a
     , "value:" <+> dprettyWithNames mempty t
     ]
diff --git a/packages/coln-compiler/test/golden/ancestor.output b/packages/coln-compiler/test/golden/ancestor.output
index 81720679..c02f5cb4 100644
--- a/packages/coln-compiler/test/golden/ancestor.output
+++ b/packages/coln-compiler/test/golden/ancestor.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named Family
+in mode: Conjunctive
 type: Theory
 value: sig
   person : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/builtin-root.output b/packages/coln-compiler/test/golden/basic-ir/builtin-root.output
index ff6d8ac2..e7361b47 100644
--- a/packages/coln-compiler/test/golden/basic-ir/builtin-root.output
+++ b/packages/coln-compiler/test/golden/basic-ir/builtin-root.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   count : Int
diff --git a/packages/coln-compiler/test/golden/basic-ir/builtin.output b/packages/coln-compiler/test/golden/basic-ir/builtin.output
index a12f33d8..a3869139 100644
--- a/packages/coln-compiler/test/golden/basic-ir/builtin.output
+++ b/packages/coln-compiler/test/golden/basic-ir/builtin.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/empty-prop-record.output b/packages/coln-compiler/test/golden/basic-ir/empty-prop-record.output
index 797dd05c..4890161d 100644
--- a/packages/coln-compiler/test/golden/basic-ir/empty-prop-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/empty-prop-record.output
@@ -1,9 +1,11 @@
 -- elaborated
 global entry named Truth
+in mode: Conjunctive
 type: Prop
 value: sig
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   truth : Truth
diff --git a/packages/coln-compiler/test/golden/basic-ir/empty-record.output b/packages/coln-compiler/test/golden/basic-ir/empty-record.output
index f22be40e..c0c5b519 100644
--- a/packages/coln-compiler/test/golden/basic-ir/empty-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/empty-record.output
@@ -1,9 +1,11 @@
 -- elaborated
 global entry named Unit
+in mode: Conjunctive
 type: Set
 value: sig
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   unit : Unit
diff --git a/packages/coln-compiler/test/golden/basic-ir/empty-theory.output b/packages/coln-compiler/test/golden/basic-ir/empty-theory.output
index 9b3bdce1..7bb1832e 100644
--- a/packages/coln-compiler/test/golden/basic-ir/empty-theory.output
+++ b/packages/coln-compiler/test/golden/basic-ir/empty-theory.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
 end
diff --git a/packages/coln-compiler/test/golden/basic-ir/equality-prop.output b/packages/coln-compiler/test/golden/basic-ir/equality-prop.output
index 978fcd5e..8cc6e1c4 100644
--- a/packages/coln-compiler/test/golden/basic-ir/equality-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/equality-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   P : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/equality.output b/packages/coln-compiler/test/golden/basic-ir/equality.output
index 63a31ab1..0c0586ac 100644
--- a/packages/coln-compiler/test/golden/basic-ir/equality.output
+++ b/packages/coln-compiler/test/golden/basic-ir/equality.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-prop.output b/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-prop.output
index 86d11401..b0977e79 100644
--- a/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-set.output b/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-set.output
index 79b5d018..982cd26b 100644
--- a/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/foreign-key-prop-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/foreign-key-set-prop.output b/packages/coln-compiler/test/golden/basic-ir/foreign-key-set-prop.output
index f6042360..ccfae4b4 100644
--- a/packages/coln-compiler/test/golden/basic-ir/foreign-key-set-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/foreign-key-set-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/foreign-key.output b/packages/coln-compiler/test/golden/basic-ir/foreign-key.output
index f5b93506..3db52628 100644
--- a/packages/coln-compiler/test/golden/basic-ir/foreign-key.output
+++ b/packages/coln-compiler/test/golden/basic-ir/foreign-key.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/function-mixed-prop-set.output b/packages/coln-compiler/test/golden/basic-ir/function-mixed-prop-set.output
index 15cf11c3..7b209e87 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function-mixed-prop-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function-mixed-prop-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/function-multi-argument.output b/packages/coln-compiler/test/golden/basic-ir/function-multi-argument.output
index f870d9ec..2b424006 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function-multi-argument.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function-multi-argument.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/function-prop-prop.output b/packages/coln-compiler/test/golden/basic-ir/function-prop-prop.output
index 78462a24..c10c115c 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function-prop-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function-prop-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/function-prop-set.output b/packages/coln-compiler/test/golden/basic-ir/function-prop-set.output
index bf875d89..9dc2aa9e 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function-prop-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function-prop-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/function-set-prop.output b/packages/coln-compiler/test/golden/basic-ir/function-set-prop.output
index 3cd5ce06..75659a87 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function-set-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function-set-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/function.output b/packages/coln-compiler/test/golden/basic-ir/function.output
index 0d46eb77..94516841 100644
--- a/packages/coln-compiler/test/golden/basic-ir/function.output
+++ b/packages/coln-compiler/test/golden/basic-ir/function.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-builtin.output b/packages/coln-compiler/test/golden/basic-ir/lookup-builtin.output
index e4b33221..cd18a07c 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-builtin.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-builtin.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-composition-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-composition-prop.output
index ceec7b16..c3ff7136 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-composition-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-composition-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-composition.output b/packages/coln-compiler/test/golden/basic-ir/lookup-composition.output
index ede8104b..58b20987 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-composition.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-composition.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-literal-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-literal-prop.output
index fc668834..11ca4a26 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-literal-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-literal-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   IntFact : Int -> Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-literal.output b/packages/coln-compiler/test/golden/basic-ir/lookup-literal.output
index 53a8a6e8..a46dff39 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-literal.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-literal.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   IntEdge : Int -> Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-prop.output
index 7e1d98a3..e8bf3176 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-set.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-set.output
index 8b099309..f355b95b 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-prop-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-prop.output
index 2423f783..481b16fd 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-set.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-set.output
index 59dc0dd5..9cc681da 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-prop-set-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-prop.output
index 565b5a6b..eddc419e 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-set.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-set.output
index ba638feb..f92c6586 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-prop-set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-set-prop.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-set-prop.output
index 9e4137e2..01e37dc6 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-set-prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection-set-set-prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-projection.output b/packages/coln-compiler/test/golden/basic-ir/lookup-projection.output
index 31f12076..412d60c6 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-projection.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-projection.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-record-composition.output b/packages/coln-compiler/test/golden/basic-ir/lookup-record-composition.output
index afc5c9fb..a38f6a85 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-record-composition.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-record-composition.output
@@ -1,15 +1,18 @@
 -- elaborated
 global entry named Key
+in mode: Conjunctive
 type: Set
 value: sig
   rank : Int
 end
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-record-expansion.output b/packages/coln-compiler/test/golden/basic-ir/lookup-record-expansion.output
index f87ded8b..bf60c3c2 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-record-expansion.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-record-expansion.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
   rank : Int
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-record-field.output b/packages/coln-compiler/test/golden/basic-ir/lookup-record-field.output
index 5da48038..c709f749 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-record-field.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-record-field.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
   rank : Int
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/lookup-record.output b/packages/coln-compiler/test/golden/basic-ir/lookup-record.output
index 39e28cb6..343bc716 100644
--- a/packages/coln-compiler/test/golden/basic-ir/lookup-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/lookup-record.output
@@ -1,14 +1,17 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
   rank : Int
 end
 global entry named fixed
+in mode: Conjunctive
 type: Payload
 value: [name := "fixed", rank := 1]
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   E : Payload -> Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-record-concrete.output b/packages/coln-compiler/test/golden/basic-ir/param-record-concrete.output
index 2ca90fd4..5e902b42 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-record-concrete.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-record-concrete.output
@@ -1,15 +1,18 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
 end
 global entry named Box
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   value : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   boxed : Box Payload -> Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-record-model.output b/packages/coln-compiler/test/golden/basic-ir/param-record-model.output
index 0f4b510f..dfb83e32 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-record-model.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-record-model.output
@@ -1,21 +1,25 @@
 -- elaborated
 global entry named Model
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
 end
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
 end
 global entry named Box
+in mode: Conjunctive
 type: (M : Model) -> (Y : Set) -> Set
 value: M => Y => sig
   modelValue : M.X
   value : Y
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   model : Model
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-record-nested.output b/packages/coln-compiler/test/golden/basic-ir/param-record-nested.output
index 43af4248..9de21eae 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-record-nested.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-record-nested.output
@@ -1,16 +1,19 @@
 -- elaborated
 global entry named Box
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   value : X
 end
 global entry named Nested
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   inner : Box X
   sibling : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-record.output b/packages/coln-compiler/test/golden/basic-ir/param-record.output
index 1fd96246..e0234631 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-record.output
@@ -1,10 +1,12 @@
 -- elaborated
 global entry named Box
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   value : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-theory-model.output b/packages/coln-compiler/test/golden/basic-ir/param-theory-model.output
index a3e83bf5..50f9933d 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-theory-model.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-theory-model.output
@@ -1,15 +1,18 @@
 -- elaborated
 global entry named Model
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
 end
 global entry named PointOf
+in mode: Conjunctive
 type: (M : Model) -> Theory
 value: M => sig
   point : M.X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   model : Model
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-theory-nested.output b/packages/coln-compiler/test/golden/basic-ir/param-theory-nested.output
index 9cbece3f..6df8abd0 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-theory-nested.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-theory-nested.output
@@ -1,15 +1,18 @@
 -- elaborated
 global entry named PointOf
+in mode: Conjunctive
 type: (X : Set) -> Theory
 value: X => sig
   point : X
 end
 global entry named Pointed
+in mode: Conjunctive
 type: (X : Set) -> Theory
 value: X => sig
   inner : PointOf X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/param-theory.output b/packages/coln-compiler/test/golden/basic-ir/param-theory.output
index fc890cbc..f16fc075 100644
--- a/packages/coln-compiler/test/golden/basic-ir/param-theory.output
+++ b/packages/coln-compiler/test/golden/basic-ir/param-theory.output
@@ -1,10 +1,12 @@
 -- elaborated
 global entry named PointOf
+in mode: Conjunctive
 type: (X : Set) -> Theory
 value: X => sig
   point : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/projection.output b/packages/coln-compiler/test/golden/basic-ir/projection.output
index e7ec4a1e..7fb6bbd7 100644
--- a/packages/coln-compiler/test/golden/basic-ir/projection.output
+++ b/packages/coln-compiler/test/golden/basic-ir/projection.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   first : X
   second : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/proof-record-mixed.output b/packages/coln-compiler/test/golden/basic-ir/proof-record-mixed.output
index 240caa01..1db84b7f 100644
--- a/packages/coln-compiler/test/golden/basic-ir/proof-record-mixed.output
+++ b/packages/coln-compiler/test/golden/basic-ir/proof-record-mixed.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named EqualTriple
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   first : X
@@ -8,6 +9,7 @@ value: X => sig
   trailing : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/proof-record-parameter.output b/packages/coln-compiler/test/golden/basic-ir/proof-record-parameter.output
index 82de7ce1..ca155bc8 100644
--- a/packages/coln-compiler/test/golden/basic-ir/proof-record-parameter.output
+++ b/packages/coln-compiler/test/golden/basic-ir/proof-record-parameter.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named EqualTriple
+in mode: Conjunctive
 type: (X : Set) -> Set
 value: X => sig
   first : X
@@ -8,6 +9,7 @@ value: X => sig
   trailing : X
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/proof-record.coln b/packages/coln-compiler/test/golden/basic-ir/proof-record.coln
index 89844234..3ac8728f 100644
--- a/packages/coln-compiler/test/golden/basic-ir/proof-record.coln
+++ b/packages/coln-compiler/test/golden/basic-ir/proof-record.coln
@@ -4,7 +4,7 @@ end
 
 theory T := sig
   X : Set
-  witness : (x : X) -> Witness X x
+  witness : (^c x : X) -> Witness X x
 end
 
 realm TRealm @ T
diff --git a/packages/coln-compiler/test/golden/basic-ir/proof-record.output b/packages/coln-compiler/test/golden/basic-ir/proof-record.output
index bbe47ee9..d0be92b4 100644
--- a/packages/coln-compiler/test/golden/basic-ir/proof-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/proof-record.output
@@ -1,10 +1,12 @@
 -- elaborated
 global entry named Witness
+in mode: Conjunctive
 type: (X : Set) -> (x : X) -> Set
 value: X => x => sig
   proof : x = x
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/prop-multi-argument.output b/packages/coln-compiler/test/golden/basic-ir/prop-multi-argument.output
index 2c0df80e..9b51f62a 100644
--- a/packages/coln-compiler/test/golden/basic-ir/prop-multi-argument.output
+++ b/packages/coln-compiler/test/golden/basic-ir/prop-multi-argument.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/prop-record.output b/packages/coln-compiler/test/golden/basic-ir/prop-record.output
index 0b1afcb4..26c83c86 100644
--- a/packages/coln-compiler/test/golden/basic-ir/prop-record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/prop-record.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named And
+in mode: Conjunctive
 type: (P : Prop) -> (Q : Prop) -> Prop
 value: P => Q => sig
   left : P
   right : Q
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   P : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/prop.output b/packages/coln-compiler/test/golden/basic-ir/prop.output
index e54fbb16..00286c00 100644
--- a/packages/coln-compiler/test/golden/basic-ir/prop.output
+++ b/packages/coln-compiler/test/golden/basic-ir/prop.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Prop
diff --git a/packages/coln-compiler/test/golden/basic-ir/record-field-order.output b/packages/coln-compiler/test/golden/basic-ir/record-field-order.output
index c2db09cf..776f7187 100644
--- a/packages/coln-compiler/test/golden/basic-ir/record-field-order.output
+++ b/packages/coln-compiler/test/golden/basic-ir/record-field-order.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named Pair
+in mode: Conjunctive
 type: Set
 value: sig
   first : Int
   second : Int
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   E : Int -> Int -> Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/record.output b/packages/coln-compiler/test/golden/basic-ir/record.output
index 5b1ea068..ee5e7338 100644
--- a/packages/coln-compiler/test/golden/basic-ir/record.output
+++ b/packages/coln-compiler/test/golden/basic-ir/record.output
@@ -1,11 +1,13 @@
 -- elaborated
 global entry named Payload
+in mode: Conjunctive
 type: Set
 value: sig
   name : String
   rank : Int
 end
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   point : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/repeated-binders.output b/packages/coln-compiler/test/golden/basic-ir/repeated-binders.output
index ed5d0ee0..08a33de8 100644
--- a/packages/coln-compiler/test/golden/basic-ir/repeated-binders.output
+++ b/packages/coln-compiler/test/golden/basic-ir/repeated-binders.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/rule-literals.output b/packages/coln-compiler/test/golden/basic-ir/rule-literals.output
index 30ac2203..7b2ad8a5 100644
--- a/packages/coln-compiler/test/golden/basic-ir/rule-literals.output
+++ b/packages/coln-compiler/test/golden/basic-ir/rule-literals.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/set.output b/packages/coln-compiler/test/golden/basic-ir/set.output
index 02750de5..b7a9cccb 100644
--- a/packages/coln-compiler/test/golden/basic-ir/set.output
+++ b/packages/coln-compiler/test/golden/basic-ir/set.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named T
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/basic-ir/theory-alias.output b/packages/coln-compiler/test/golden/basic-ir/theory-alias.output
index bbaa0e75..a4b174a1 100644
--- a/packages/coln-compiler/test/golden/basic-ir/theory-alias.output
+++ b/packages/coln-compiler/test/golden/basic-ir/theory-alias.output
@@ -1,10 +1,12 @@
 -- elaborated
 global entry named Base
+in mode: Conjunctive
 type: Theory
 value: sig
   X : Set
 end
 global entry named Alias
+in mode: Conjunctive
 type: Theory
 value: Base
 realm named TRealm
diff --git a/packages/coln-compiler/test/golden/elaborator-errors.output b/packages/coln-compiler/test/golden/elaborator-errors.output
index 89a00509..ed36d1c0 100644
--- a/packages/coln-compiler/test/golden/elaborator-errors.output
+++ b/packages/coln-compiler/test/golden/elaborator-errors.output
@@ -1,31 +1,37 @@
 -- elaborated
 global entry named Pair
+in mode: Conjunctive
 type: Set
 value: sig
   first : Int
   second : Int
 end
 global entry named pair
+in mode: Conjunctive
 type: Pair
 value: [first := 1, second := 2]
 global entry named Dependent
+in mode: Conjunctive
 type: Theory
 value: sig
   A : Set
   value : A
 end
 global entry named dependent
+in mode: Conjunctive
 type: Dependent
 value: [A := Int, value := 1]
-global entry named identity
-type: Int -> Int
-value: x => x
-global entry named shadow
-type: (x : String) -> Int -> Int
-value: x => x => x
 
 -- messages
 
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+21 | def identity : Int -> Int := x => x
+21 |                                   ^
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+23 | def shadow (x : String) : Int -> Int := x => x
+23 |                                              ^
+
 error[E0302]: tried to project from a value that was not of a record type
 25 | def projectionOfNonRecord : Int := (1).missing
 25 |                                       ^^^^^^^^
diff --git a/packages/coln-compiler/test/golden/equality.coln b/packages/coln-compiler/test/golden/equality.coln
new file mode 100644
index 00000000..118bc1f7
--- /dev/null
+++ b/packages/coln-compiler/test/golden/equality.coln
@@ -0,0 +1,6 @@
+theory ReflexiveRelation (^i X : Set) := sig
+  rel : (^i x : X) -> (^i y : X) -> Prop
+  refl : (^i x : X) -> rel x x
+end
+
+ind def Eq (X : Set) : ReflexiveRelation X := init (ReflexiveRelation X)
diff --git a/packages/coln-compiler/test/golden/equality.output b/packages/coln-compiler/test/golden/equality.output
new file mode 100644
index 00000000..0826d3f6
--- /dev/null
+++ b/packages/coln-compiler/test/golden/equality.output
@@ -0,0 +1,14 @@
+-- elaborated
+global entry named ReflexiveRelation
+in mode: Conjunctive
+type: (X : Set) -> Theory
+value: X => sig
+  rel : (x : X) -> (y : X) -> Prop
+  refl : (x : X) -> rel x x
+end
+global entry named Eq
+in mode: Inductive
+type: (X : Set) -> ReflexiveRelation X
+value: X => init (ReflexiveRelation X)
+
+-- messages
diff --git a/packages/coln-compiler/test/golden/fb3.output b/packages/coln-compiler/test/golden/fb3.output
index 168a03b6..7d714b29 100644
--- a/packages/coln-compiler/test/golden/fb3.output
+++ b/packages/coln-compiler/test/golden/fb3.output
@@ -1,11 +1,8 @@
 -- elaborated
-global entry named IdempotentSemigroup
-type: Theory
-value: sig
-  Element : Set
-  mul : (x : Element) -> (y : Element) -> Element
-  mul/idempotent : (x : Element) -> mul x x = x
-  mul/assoc : (x : Element) -> (y : Element) -> (z : Element) -> mul (mul x y) z = mul x (mul y z)
-end
+
 
 -- messages
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+7 |   mul/idempotent : (x : Element) -> mul x x = x
+7 |                                               ^
diff --git a/packages/coln-compiler/test/golden/graph-of-graphs.output b/packages/coln-compiler/test/golden/graph-of-graphs.output
index 7c1c670c..63d1ce8d 100644
--- a/packages/coln-compiler/test/golden/graph-of-graphs.output
+++ b/packages/coln-compiler/test/golden/graph-of-graphs.output
@@ -1,17 +1,20 @@
 -- elaborated
 global entry named Graph
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
   E : V -> V -> Set
 end
 global entry named Graph/hom
+in mode: Conjunctive
 type: (G0 : Graph) -> (G1 : Graph) -> Theory
 value: G0 => G1 => sig
   V : G0.V -> G1.V
   E : (v0 : G0.V) -> (v1 : G0.V) -> G0.E v0 v1 -> G1.E (V v0) (V v1)
 end
 global entry named GraphOfGraphs
+in mode: Conjunctive
 type: Theory
 value: sig
   base : Graph
diff --git a/packages/coln-compiler/test/golden/graph.output b/packages/coln-compiler/test/golden/graph.output
index 960be3c5..048dac1b 100644
--- a/packages/coln-compiler/test/golden/graph.output
+++ b/packages/coln-compiler/test/golden/graph.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named Graph
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
diff --git a/packages/coln-compiler/test/golden/hlevel.output b/packages/coln-compiler/test/golden/hlevel.output
index 9325a41b..80e29d42 100644
--- a/packages/coln-compiler/test/golden/hlevel.output
+++ b/packages/coln-compiler/test/golden/hlevel.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named Family
+in mode: Conjunctive
 type: Theory
 value: sig
   person : Set
@@ -7,12 +8,14 @@ value: sig
   happy : Prop
 end
 global entry named Q
+in mode: Conjunctive
 type: (F : Family) -> Theory
 value: F => sig
   son : F.person
   father : F.person
 end
 global entry named HP
+in mode: Conjunctive
 type: Theory
 value: sig
   person : Set
@@ -21,10 +24,12 @@ value: sig
   reveal : voldemort = tomriddle
 end
 global entry named Unit
+in mode: Conjunctive
 type: Prop
 value: sig
 end
 global entry named P
+in mode: Conjunctive
 type: Theory
 value: sig
   u : Unit
diff --git a/packages/coln-compiler/test/golden/ind.coln b/packages/coln-compiler/test/golden/ind.coln
new file mode 100644
index 00000000..01b70216
--- /dev/null
+++ b/packages/coln-compiler/test/golden/ind.coln
@@ -0,0 +1,14 @@
+theory Graph := sig
+  v : Set
+  e : v -> v -> Prop
+end
+
+theory TransitiveExt (^i G : Graph) := sig
+  p : G.v -> G.v -> Prop
+  incl : (v0 : G.v) -> (v1 : G.v) -> G.e v0 v1 -> p v0 v1
+  snoc : (v0 : G.v) -> (v1 : G.v) -> (v2 : G.v) -> p v0 v1 -> G.e v1 v2 -> p v0 v2
+end
+
+ind def transitive-closure (G : Graph) : TransitiveExt G := init (TransitiveExt G)
+
+ind def free-point (X : Set) : X := init X
diff --git a/packages/coln-compiler/test/golden/ind.output b/packages/coln-compiler/test/golden/ind.output
new file mode 100644
index 00000000..28758444
--- /dev/null
+++ b/packages/coln-compiler/test/golden/ind.output
@@ -0,0 +1,26 @@
+-- elaborated
+global entry named Graph
+in mode: Conjunctive
+type: Theory
+value: sig
+  v : Set
+  e : v -> v -> Prop
+end
+global entry named TransitiveExt
+in mode: Conjunctive
+type: (G : Graph) -> Theory
+value: G => sig
+  p : G.v -> G.v -> Prop
+  incl : (v0 : G.v) -> (v1 : G.v) -> G.e v0 v1 -> p v0 v1
+  snoc : (v0 : G.v) -> (v1 : G.v) -> (v2 : G.v) -> p v0 v1 -> G.e v1 v2 -> p v0 v2
+end
+global entry named transitive-closure
+in mode: Inductive
+type: (G : Graph) -> TransitiveExt G
+value: G => init (TransitiveExt G)
+
+-- messages
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+14 | ind def free-point (X : Set) : X := init X
+14 |                                          ^
diff --git a/packages/coln-compiler/test/golden/lambda.output b/packages/coln-compiler/test/golden/lambda.output
index 3a944b8a..3521afb3 100644
--- a/packages/coln-compiler/test/golden/lambda.output
+++ b/packages/coln-compiler/test/golden/lambda.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named Lambda
+in mode: Conjunctive
 type: Theory
 value: sig
   con : Set
diff --git a/packages/coln-compiler/test/golden/magma.output b/packages/coln-compiler/test/golden/magma.output
index 5f8fc089..273ebd56 100644
--- a/packages/coln-compiler/test/golden/magma.output
+++ b/packages/coln-compiler/test/golden/magma.output
@@ -1,5 +1,6 @@
 -- elaborated
 global entry named Magma
+in mode: Conjunctive
 type: Theory
 value: sig
   car : Set
diff --git a/packages/coln-compiler/test/golden/modular-lattice.output b/packages/coln-compiler/test/golden/modular-lattice.output
index add4021f..d77628e3 100644
--- a/packages/coln-compiler/test/golden/modular-lattice.output
+++ b/packages/coln-compiler/test/golden/modular-lattice.output
@@ -1,23 +1,12 @@
 -- elaborated
-global entry named ModularLattice
-type: Theory
-value: sig
-  Element : Set
-  meet : Element -> Element -> Element
-  meet/associative : (a : Element) -> (b : Element) -> (c : Element) -> meet (meet a b) c = meet a (meet b c)
-  meet/commutative : (a : Element) -> (b : Element) -> meet a b = meet b a
-  meet/idempotent : (a : Element) -> meet a a = a
-  join : Element -> Element -> Element
-  join/associative : (a : Element) -> (b : Element) -> (c : Element) -> join (join a b) c = join a (join b c)
-  join/associative : (a : Element) -> (b : Element) -> join a b = join b a
-  join/idempotent : (a : Element) -> join a a = a
-  ax/absorptive1 : (a : Element) -> (b : Element) -> meet a (join a b) = a
-  ax/absorptive2 : (a : Element) -> (b : Element) -> join a (meet a b) = a
-  ax/modular : (a : Element) -> (b : Element) -> (x : Element) -> join (meet a b) (meet x b) = meet (join (meet a b) x) b
-end
+
 
 -- messages
 
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+17 |     meet a a = a
+17 |                ^
+
 error[E0200]: unexpected notation for field setting of the form `<fieldname> := <expr>`: Infix
 49 |     bot : Element                                                                                                        
 49 |     ^^^^^^^^^^^^^
diff --git a/packages/coln-compiler/test/golden/monoid-glog.output b/packages/coln-compiler/test/golden/monoid-glog.output
index 808c3322..83ab7ebc 100644
--- a/packages/coln-compiler/test/golden/monoid-glog.output
+++ b/packages/coln-compiler/test/golden/monoid-glog.output
@@ -1,13 +1,8 @@
 -- elaborated
-global entry named Monoid
-type: Theory
-value: sig
-  car : Set
-  unit : car
-  mul : car -> car -> car
-  mul/unitl : (x : car) -> mul unit x = x
-  mul/unitr : (x : car) -> mul x unit = x
-  mul/assoc : (x : car) -> (y : car) -> (z : car) -> mul (mul x y) z = mul x (mul y z)
-end
+
 
 -- messages
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+6 |   mul/unitl : (x : car) -> mul unit x = x
+6 |                                         ^
diff --git a/packages/coln-compiler/test/golden/nominal.output b/packages/coln-compiler/test/golden/nominal.output
index 9ef78e08..cc083644 100644
--- a/packages/coln-compiler/test/golden/nominal.output
+++ b/packages/coln-compiler/test/golden/nominal.output
@@ -1,13 +1,16 @@
 -- elaborated
 global entry named A
+in mode: Conjunctive
 type: Theory
 value: sig
 end
 global entry named B
+in mode: Conjunctive
 type: Theory
 value: sig
 end
 global entry named a
+in mode: Conjunctive
 type: A
 value: []
 
diff --git a/packages/coln-compiler/test/golden/paths.coln b/packages/coln-compiler/test/golden/paths.coln
index 75c44239..d5fb01ec 100644
--- a/packages/coln-compiler/test/golden/paths.coln
+++ b/packages/coln-compiler/test/golden/paths.coln
@@ -16,6 +16,8 @@ theory Reachability/motive (G : Graph) := sig
   )
 end
 
+
+
 realm Graph @ Graph
   ind def reachability : Reachability/motive self := init (Reachability/motive self)
 end
diff --git a/packages/coln-compiler/test/golden/paths.output b/packages/coln-compiler/test/golden/paths.output
index a3ee8f95..24701861 100644
--- a/packages/coln-compiler/test/golden/paths.output
+++ b/packages/coln-compiler/test/golden/paths.output
@@ -1,26 +1,36 @@
 -- elaborated
 global entry named Graph
+in mode: Conjunctive
 type: Theory
 value: sig
   V : Set
   E : V -> V -> Prop
 end
 global entry named Reachability/motive
+in mode: Conjunctive
 type: (G : Graph) -> Theory
 value: G => sig
   t : G.V -> G.V -> Prop
   empty : (x : G.V) -> t x x
   cons : (x : G.V) -> (y : G.V) -> (z : G.V) -> (e : G.E x y) -> t y z -> t x z
 end
+realm named Graph
+generators: node
+  V = rel []
+  E = rel [a : Graph.V [], b : Graph.V []]
+end
+lowered: flatrealm
+  entities
+    table ℜ.V := []
+    table ℜ.E := [.a : ℜ.V, .b : ℜ.V]
+  end
+  rules
+    enforced ℜ.V.foreignKey := ℜ.V [] ⊢ ⊤
+    enforced ℜ.E.foreignKey a b := ℜ.E [
+      .a ↦ a,
+      .b ↦ b
+    ] ⊢ a ∈ ℜ.V [] ∧ b ∈ ℜ.V []
+  end
+end
 
 -- messages
-
-error[E0104]: expected a newline, end, or eof after a statement
-20 |   ind def reachability : Reachability/motive self := init (Reachability/motive self)
-20 |       ^^^
-
-error[E0200]: unexpected notation for top-level declaration: Infix
-19 | realm Graph @ Graph
-19 | ^^^^^^^^^^^^^^^^^^^
-20 |   ind def reachability : Reachability/motive self := init (Reachability/motive self)
-20 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/packages/coln-compiler/test/golden/ssa.output b/packages/coln-compiler/test/golden/ssa.output
index 46a54dae..e6c60421 100644
--- a/packages/coln-compiler/test/golden/ssa.output
+++ b/packages/coln-compiler/test/golden/ssa.output
@@ -1,69 +1,46 @@
 -- elaborated
 global entry named IsTransClosure
+in mode: Conjunctive
 type: (X : Set) -> (R : X -> X -> Set) -> (P : X -> X -> Set) -> Theory
 value: X => R => P => sig
   refl : (x : X) -> P x x
   snoc : (x : X) -> (y : X) -> (z : X) -> P x y -> R y z -> P x z
 end
-global entry named LinearOrder
-type: Theory
-value: sig
-  car : Set
-  first : car
-  last : car
-  next : car -> car
-  prev : car -> car
-  next/prev : (x : car) -> next (prev x) = x
-  prev/next : (x : car) -> prev (next x) = x
-  follows : car -> car -> Set
-  follows/is-trans-closure : IsTransClosure car (x => y => next x = y) follows
-  acyclic : (x : car) -> (y : car) -> follows x y -> follows y x -> x = y
-  first-is-top : (x : car) -> follows first x
-  last-is-bot : (x : car) -> follows x last
-end
 global entry named OpInfo
+in mode: Conjunctive
 type: Theory
 value: sig
   OpType : Set
   inputArity : OpType -> Set
   outputArity : OpType -> Set
 end
-global entry named Iso
-type: (A : Set) -> (B : Set) -> Theory
-value: A => B => sig
-  fwd : A -> B
-  bwd : B -> A
-  fwd/bwd : (a : A) -> bwd (fwd a) = a
-  bwd/fwd : (b : B) -> fwd (bwd b) = b
-end
-global entry named Operation
-type: (opInfo : OpInfo) -> (val : Set) -> (outputs : Set) -> Theory
-value: opInfo => val => outputs => sig
-  opType : opInfo.OpType
-  opInputs : opInfo.inputArity opType -> val
-  opOutputs : Iso outputs (opInfo.outputArity opType)
-end
 global entry named PrecedingOutput
+in mode: Conjunctive
 type: (X : Set) -> (rel : X -> X -> Set) -> (x : X) -> (outputs : X -> Set) -> Set
 value: X => rel => x => outputs => sig
   y : X
   isPreceding : rel y x
   output : outputs y
 end
-global entry named Block
-type: (opInfo : OpInfo) -> Theory
-value: opInfo => sig
-  ops : LinearOrder
-  outputs : ops.car -> Set
-  payload : (x : ops.car) -> Operation opInfo (PrecedingOutput ops.car ops.follows x outputs) (outputs x)
-  args : LinearOrder
-end
-global entry named SSA
-type: (opInfo : OpInfo) -> Theory
-value: opInfo => sig
-  RegionId : Set
-  BlockId : RegionId -> Set
-  ops : (r : RegionId) -> BlockId r -> Block opInfo
-end
 
 -- messages
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+13 |   next/prev : (x : car) -> next (prev x) = x
+13 |                                            ^
+
+error[E0316]: cannot use inductively bound variable in a conjunctive context
+34 |   fwd/bwd : (a : A) -> bwd (fwd a) = a
+34 |                                      ^
+
+error[E0314]: no such variable Iso in scope
+41 |   opOutputs : Iso outputs (opInfo.outputArity opType)
+41 |               ^^^
+
+error[E0314]: no such variable LinearOrder in scope
+51 |   ops : LinearOrder
+51 |         ^^^^^^^^^^^
+
+error[E0314]: no such variable Block in scope
+65 |   ops : (r : RegionId) -> BlockId r -> Block opInfo
+65 |                                        ^^^^^
diff --git a/packages/coln-repl/src/Coln/REPL.hs b/packages/coln-repl/src/Coln/REPL.hs
index 6e7a6d93..07b42a56 100644
--- a/packages/coln-repl/src/Coln/REPL.hs
+++ b/packages/coln-repl/src/Coln/REPL.hs
@@ -6,14 +6,14 @@ module Coln.REPL (runRepl) where
 
 import Coln.Common
 import Coln.Core.Globals
-import Coln.Core.Params (CtxShape (..), N)
+import Coln.Core.Params (CtxShape (..), Mode (..), N)
 import Coln.Core.Print (DPrettyWithNames (dprettyWithNames), prtIn)
 import Coln.Core.Realm (Realm)
 import Coln.Diagnostics
 import Coln.Elaborator.Environment (emptyElabEnv)
 import Coln.Elaborator.Judgment (Syn (..))
 import Coln.Frontend.Notation
-import Coln.Frontend.Parser (decl', syn)
+import Coln.Frontend.Parser (decl, syn)
 import Control.Monad
 import Control.Monad.State.Strict
 import Control.Monad.Writer
@@ -81,15 +81,15 @@ eval file = do
     case ntn of
       -- register declaration
       Decl name _ _ -> do
-        put =<< liftIO (decl' diagEnv ge ntn)
+        put =<< liftIO (decl diagEnv ge ntn)
         tell [name]
       -- ignore realms
       Block "realm" _ _ _ -> pure ()
       -- evaluate expression
       _ ->
         liftIO do
-          let elabEnv = emptyElabEnv (envFor ElaboratorCode) ge
-          ntnSyn <- (syn @N) diagEnv "" ntn
+          let elabEnv = emptyElabEnv (envFor ElaboratorCode) ge Conjunctive
+          ntnSyn <- (syn @N) (contramap ParserCode diagEnv) "" ntn
           (t, m) <- ntnSyn.elab elabEnv
           putDoc $ prtIn elabEnv m <+> ":" <+> prtIn elabEnv t <+> "\n"
 
@@ -100,7 +100,7 @@ eval file = do
   reporter translator = contramap translator $ terminalReporter stdout
 
 prettyEntry :: (Name, GlobalEntry) -> DDoc
-prettyEntry (x, GlobalEntry t _ a) =
+prettyEntry (x, GlobalEntry t _ a _) =
   vsep
     [ "global entry named" <+> dpretty x
     , "type:" <+> prtIn (CtxShape 0 BwdNil) a
diff --git a/packages/fnotation/src/FNotation/Kinds.hs b/packages/fnotation/src/FNotation/Kinds.hs
index 7be62f2d..d8d5eea4 100644
--- a/packages/fnotation/src/FNotation/Kinds.hs
+++ b/packages/fnotation/src/FNotation/Kinds.hs
@@ -24,6 +24,7 @@ data Kind
   | Field
   | -- | No-space field, like the `x` in `f.x`
     FieldImmediate
+  | Mode
   | Int
   | String
   | LParen
diff --git a/packages/fnotation/src/FNotation/Lexer.hs b/packages/fnotation/src/FNotation/Lexer.hs
index 8408df4d..ae3892d0 100644
--- a/packages/fnotation/src/FNotation/Lexer.hs
+++ b/packages/fnotation/src/FNotation/Lexer.hs
@@ -320,6 +320,7 @@ run st fresh =
     '\"' -> string st >> run st False
     '.' -> advance st >> tryName st (if fresh then Field else FieldImmediate) "period" >> run st False
     '\'' -> advance st >> tryName st Tag "single quote" >> run st False
+    '^' -> advance st >> tryName st Mode "at sign" >> run st False
     '\0' -> emit0 st Eof
     '`' -> ident st >> run st False
     c | isDigit c -> (int st >>= emit st Int . VInt) >> run st False
diff --git a/packages/fnotation/src/FNotation/Pretty.hs b/packages/fnotation/src/FNotation/Pretty.hs
index 04ea4348..4ed8cb7a 100644
--- a/packages/fnotation/src/FNotation/Pretty.hs
+++ b/packages/fnotation/src/FNotation/Pretty.hs
@@ -92,6 +92,7 @@ prt p = \case
   Keyword x _ -> dpretty x
   Field x _ -> "." <> dprettyWithKinds ?lconfig x
   Tag x _ -> "'" <> dprettyWithKinds ?lconfig x
+  Mode x _ -> "^" <> dprettyWithKinds ?lconfig x
   Int i _ -> pretty i
   String x _ -> "\"" <> pretty x <> "\""
   Tuple ns _ -> bracketedTuple $ prtTop <$> ns
diff --git a/packages/fnotation/src/FNotation/Reader.hs b/packages/fnotation/src/FNotation/Reader.hs
index becdb30b..b213a886 100644
--- a/packages/fnotation/src/FNotation/Reader.hs
+++ b/packages/fnotation/src/FNotation/Reader.hs
@@ -181,6 +181,7 @@ argStarts =
     , T.AKeyword
     , T.Field
     , T.Tag
+    , T.Mode
     , T.Int
     , T.String
     , T.Block
@@ -236,6 +237,9 @@ argBase st = do
     T.Tag -> do
       x <- curName st
       advanceClose st m $ Tag x
+    T.Mode -> do
+      x <- curName st
+      advanceClose st m $ Mode x
     T.Int -> do
       i <- curInt st
       advanceClose st m $ Int i
diff --git a/packages/fnotation/src/FNotation/Trees.hs b/packages/fnotation/src/FNotation/Trees.hs
index 54b66c1f..ad9738c4 100644
--- a/packages/fnotation/src/FNotation/Trees.hs
+++ b/packages/fnotation/src/FNotation/Trees.hs
@@ -37,6 +37,7 @@ data NtnGeneric a
   | Keyword Name a
   | Field Name a
   | Tag Name a
+  | Mode Name a
   | Int Int a
   | String Text a
   | Error a
@@ -68,6 +69,7 @@ startPos (Ident _ s) = s.start
 startPos (Keyword _ s) = s.start
 startPos (Field _ s) = s.start
 startPos (Tag _ s) = s.start
+startPos (Mode _ s) = s.start
 startPos (Int _ s) = s.start
 startPos (String _ s) = s.start
 startPos (Tuple _ s) = s.start
@@ -82,6 +84,7 @@ endPos (Ident _ s) = s.end
 endPos (Keyword _ s) = s.end
 endPos (Field _ s) = s.end
 endPos (Tag _ s) = s.end
+endPos (Mode _ s) = s.end
 endPos (Int _ s) = s.end
 endPos (String _ s) = s.end
 endPos (Tuple _ s) = s.end
@@ -102,6 +105,7 @@ head (Ident x _) = "Ident" <+> dpretty x
 head (Keyword x _) = "Keyword" <+> dpretty x
 head (Field x _) = "Field" <+> dpretty x
 head (Tag x _) = "Tag" <+> dpretty x
+head (Mode x _) = "Mode" <+> dpretty x
 head (Int i _) = "Int" <+> pretty i
 head (String s _) = "String" <+> pretty s
 head (Tuple _ _) = "Tuple"
@@ -116,6 +120,7 @@ children (Ident _ _) = []
 children (Keyword _ _) = []
 children (Field _ _) = []
 children (Tag _ _) = []
+children (Mode _ _) = []
 children (Int _ _) = []
 children (String _ _) = []
 children (Tuple ns _) = ns