From a33e76fe516038ffa2c705aba99c7ca910f22b67 Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Thu, 18 Jun 2026 17:25:30 +0100
Subject: [PATCH 01/11] Initial hlevels work

---
 .../coln-compiler/src/Coln/Core/Layout.hs     |  4 +-
 .../coln-compiler/src/Coln/Core/Params.hs     | 67 ++++++++++++++-----
 packages/coln-compiler/src/Coln/Core/Print.hs |  2 +-
 packages/coln-compiler/src/Coln/Core/Value.hs |  4 +-
 .../src/Coln/Elaborator/Rules/Equality.hs     |  2 +-
 .../src/Coln/Elaborator/Rules/Function.hs     | 10 ++-
 .../src/Coln/Elaborator/Rules/Record.hs       |  4 +-
 .../coln-compiler/src/Coln/Frontend/Driver.hs |  2 +-
 packages/coln-compiler/test/ancestor.output   |  2 +-
 packages/coln-compiler/test/hlevel.glog       | 19 ++++++
 packages/coln-compiler/test/hlevel.output     | 40 +++++++++++
 11 files changed, 128 insertions(+), 28 deletions(-)
 create mode 100644 packages/coln-compiler/test/hlevel.glog
 create mode 100644 packages/coln-compiler/test/hlevel.output

diff --git a/packages/coln-compiler/src/Coln/Core/Layout.hs b/packages/coln-compiler/src/Coln/Core/Layout.hs
index 853be9a3..b28f5478 100644
--- a/packages/coln-compiler/src/Coln/Core/Layout.hs
+++ b/packages/coln-compiler/src/Coln/Core/Layout.hs
@@ -49,7 +49,7 @@ bind sc x a =
 
 layout :: Path -> Scope -> V.Ty N -> (Trie Generator, M.El N)
 layout p sc a
-  | levelOf a == Theory = case V.behavior a of
+  | (levelOf a).sort == Theory = case V.behavior a of
       V.LikeFunction ft -> do
         let x = argName sc.usedNames ft.cod
         let (v, sc') = bind sc x ft.dom
@@ -71,7 +71,7 @@ layout p sc a
         (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"
-  | levelOf a == Set = do
+  | (levelOf a).sort == Set = do
       let gt = Leaf (Fun (toList sc.names) (toList sc.ctx) (readb sc.len a))
       let v = V.Lookup (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
       (gt, M.fromVEl sc.len v)
diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index dfbb03a6..1dea486b 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -12,16 +12,16 @@ import Prettyprinter
 -- Level stuff (levels, universes, function variants)
 --------------------------------------------------------------------------------
 
-data Level
+data Sort
   = Set
   | Theory
   | Top
   deriving (Eq, Show)
 
-instance DPretty Level where
+instance DPretty Sort where
   dpretty = pretty . show
 
-instance PartialOrd Level where
+instance PartialOrd Sort where
   leq l1 l2 = case (l1, l2) of
     (Set, _) -> True
     (Theory, Set) -> False
@@ -29,6 +29,30 @@ instance PartialOrd Level where
     (Top, Top) -> True
     (Top, _) -> False
 
+maxSort :: Sort -> Sort -> Sort
+maxSort l1 l2
+  | leq l1 l2 = l2
+  | otherwise = l1
+
+data HLevel
+  = HProp
+  | HSet
+  deriving (Eq, Show)
+
+instance PartialOrd HLevel where
+  leq l1 l2 = case (l1, l2) of
+    (HProp, _) -> True
+    (HSet, HProp) -> False
+    (HSet, _) -> True
+
+data Level = Level {
+  sort :: Sort,
+  hlevel :: HLevel }
+  deriving (Eq, Show)
+
+instance PartialOrd Level where
+  leq (Level s1 h1) (Level s2 h2) = s1 `leq` s2 && h1 `leq` h2
+
 maxLevel :: Level -> Level -> Level
 maxLevel l1 l2
   | leq l1 l2 = l2
@@ -38,33 +62,44 @@ class LevelOf a where
   levelOf :: a -> Level
 
 data Universe
-  = SetU
+  = PropU
+  | SetU
   | TheoryU
+  | PropTheoryU -- TODO: better name?
   deriving (Eq, Show)
 
 decodesInto :: Universe -> Level
 decodesInto = \case
-  SetU -> Set
-  TheoryU -> Theory
+  PropU -> Level Set HProp
+  SetU -> Level Set HSet
+  PropTheoryU -> Level Theory HProp
+  TheoryU -> Level Theory HSet
 
 codesInto :: Universe -> Level
 codesInto = \case
-  SetU -> Theory
-  TheoryU -> Top
+  PropU -> Level Theory HSet
+  SetU -> Level Theory HSet
+  TheoryU -> Level Top HSet
+  PropTheoryU -> Level Top HSet
 
 instance Pretty Universe where
   pretty = \case
+    PropU -> "Prop"
     SetU -> "Set"
     TheoryU -> "Theory"
+    PropTheoryU -> "PropTheory"
 
 universeFor :: Level -> Maybe Universe
 universeFor = \case
-  Set -> Just SetU
-  Theory -> Just TheoryU
-  Top -> Nothing
+  Level Set HProp -> Just PropU
+  Level Set HSet -> Just SetU
+  Level Theory HProp -> Just PropTheoryU
+  Level Theory HSet -> Just TheoryU
+  Level Top _ -> Nothing
 
 data FunctionVariant
-  = SetTheory
+  = SetPropTheory -- TODO: better name?
+  | SetTheory
   | TheoryTop
   deriving (Eq, Show)
 
@@ -73,14 +108,16 @@ instance Pretty FunctionVariant where
 
 instance LevelOf FunctionVariant where
   levelOf = \case
-    SetTheory -> Theory
-    TheoryTop -> Top
+    SetPropTheory -> Level Theory HProp
+    SetTheory -> Level Theory HSet
+    TheoryTop -> Level Top HSet
 
 class HasCodomain a b | a -> b where
   codOf :: a -> b
 
-instance HasCodomain FunctionVariant Level where
+instance HasCodomain FunctionVariant Sort where
   codOf = \case
+    SetPropTheory -> Theory
     SetTheory -> Theory
     TheoryTop -> Top
 
diff --git a/packages/coln-compiler/src/Coln/Core/Print.hs b/packages/coln-compiler/src/Coln/Core/Print.hs
index 8821d0f1..0d2ef992 100644
--- a/packages/coln-compiler/src/Coln/Core/Print.hs
+++ b/packages/coln-compiler/src/Coln/Core/Print.hs
@@ -69,7 +69,7 @@ nbinding x n = N.Infix (N.Ident x ()) (N.Keyword ":" ()) n
 
 instance ToNotation (Ty e) where
   toNotation xs = \case
-    U u -> N.Keyword (fromString $ show $ decodesInto u) ()
+    U u -> N.Keyword (fromString $ show $ pretty u) ()
     Decode t -> toNotation xs t
     Function f -> case f.cod of
       Abs x b ->
diff --git a/packages/coln-compiler/src/Coln/Core/Value.hs b/packages/coln-compiler/src/Coln/Core/Value.hs
index 184fda9b..929251cc 100644
--- a/packages/coln-compiler/src/Coln/Core/Value.hs
+++ b/packages/coln-compiler/src/Coln/Core/Value.hs
@@ -226,8 +226,8 @@ instance LevelOf (Ty c) where
     Function ft -> levelOf ft.variant
     Record rt -> rt.level
     Eq ety -> levelOf ety.at
-    BuiltinTy _ -> Set
-    EltOf _ _ -> Set
+    BuiltinTy _ -> Level Set HSet -- Only Int/String so far
+    EltOf _ _ -> Level Set HSet -- TODO
 
 behavior :: Ty c -> TypeBehavior
 behavior = \case
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
index 82236017..c96156cb 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
@@ -28,7 +28,7 @@ formation sp lhs rhs = Typ \e -> do
       let msg = "types" <+> prtIn e lty <+> "and" <+> prtIn e rty <+> "of compared terms differ"
       let note = Just $ dpretty err
       failWithNote e.diagEnv sp TypeMismatch msg note
-    Right _ -> case levelOf lty of
+    Right _ -> case (levelOf lty).sort of
       Set -> pure $ equality $ S.EqualityType (fromVTy e.scope.len lty) elhs erhs
       _ -> do
         let msg = "equality requires data types, but" <+> prtIn e lty <+> "is a schema-level type"
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
index 9fa495e8..a7f35ba5 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
@@ -17,9 +17,13 @@ import Coln.Report
 
 variantFor :: Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
 variantFor dom cod sp e = case (levelOf dom, levelOf cod) of
-  ((Set, Set); (Set, Theory)) -> pure SetTheory
-  ((Set, Top); (Theory, _)) -> pure TheoryTop
-  (Top, _) -> do
+  (Level Set _, Level Set HProp) -> pure SetPropTheory
+  (Level Set _, Level Theory HProp) -> pure SetPropTheory
+  (Level Set _, Level Set HSet) -> pure SetTheory
+  (Level Set _, Level Theory HSet) -> pure SetTheory
+  (Level Set _, Level Top _) -> pure TheoryTop
+  (Level Theory _, Level _ _) -> pure TheoryTop
+  (Level Top _, _) -> do
     let msg = "higher-order theories are not supported"
     failWith e.diagEnv sp FunctionDomainTooLarge msg
 
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
index 5542b28d..66a27695 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
@@ -27,8 +27,8 @@ data FieldDeclaration
 
 formation :: [FieldDeclaration] -> Typ D
 formation fieldTyps = Typ $ \e -> do
-  let go _ [] = pure (Set, [])
-      go e' ((FieldDeclaration x typ) : rest) = do
+  let go _ [] = pure (Level Set HProp, [])
+      go e' ((FieldDeclaration x typ):rest) = do
         ty <- typ.elab e'
         (l, fieldTys) <- go (e'{scope = bind x ty.val e'.scope}) rest
         pure (maxLevel l (levelOf ty), (x, ty) : fieldTys)
diff --git a/packages/coln-compiler/src/Coln/Frontend/Driver.hs b/packages/coln-compiler/src/Coln/Frontend/Driver.hs
index 9d8e2826..044ad96f 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Driver.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Driver.hs
@@ -194,7 +194,7 @@ expr e n = case n of
     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 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 ->
diff --git a/packages/coln-compiler/test/ancestor.output b/packages/coln-compiler/test/ancestor.output
index d4b291f6..81720679 100644
--- a/packages/coln-compiler/test/ancestor.output
+++ b/packages/coln-compiler/test/ancestor.output
@@ -3,7 +3,7 @@ global entry named Family
 type: Theory
 value: sig
   person : Set
-  is-parent : person -> person -> Set
+  is-parent : person -> person -> Prop
 end
 
 -- messages
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.glog
new file mode 100644
index 00000000..18923b34
--- /dev/null
+++ b/packages/coln-compiler/test/hlevel.glog
@@ -0,0 +1,19 @@
+theory Family := sig
+  person : Set
+  is-parent : person -> person -> Prop
+
+  happy : Prop
+
+  showtype happy
+  showtype is-parent
+  showtype happy -> person
+  showtype person -> happy
+end
+
+theory Q (F : Family) := sig
+  son : F.person
+  father : F.person
+
+  showtype F.is-parent
+  showtype F.is-parent father son
+end
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
new file mode 100644
index 00000000..626081da
--- /dev/null
+++ b/packages/coln-compiler/test/hlevel.output
@@ -0,0 +1,40 @@
+-- elaborated
+global entry named Family
+type: Theory
+value: sig
+  person : Set
+  is-parent : person -> person -> Prop
+  happy : Prop
+end
+global entry named Q
+type: (F : Family) -> Theory
+value: F => sig
+  son : F.person
+  father : F.person
+end
+
+-- messages
+
+debug[D0315]: value happy has type Prop
+7 |   showtype happy
+7 |            ^^^^^
+
+debug[D0315]: value is-parent has type person -> person -> Prop
+8 |   showtype is-parent
+8 |            ^^^^^^^^^
+
+debug[D0315]: value happy -> person has type Theory
+9 |   showtype happy -> person
+9 |            ^^^^^^^^^^^^^^^
+
+debug[D0315]: value person -> happy has type PropTheory
+10 |   showtype person -> happy
+10 |            ^^^^^^^^^^^^^^^
+
+debug[D0315]: value F.is-parent has type F.person -> F.person -> Prop
+17 |   showtype F.is-parent
+17 |            ^^^^^^^^^^^
+
+debug[D0315]: value F.is-parent father son has type Prop
+18 |   showtype F.is-parent father son
+18 |            ^^^^^^^^^^^^^^^^^^^^^^

From 89f1e27026d2d4319d0360bde8028e650936f84e Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 11:29:59 +0100
Subject: [PATCH 02/11] Sort -> MLevel

---
 packages/coln-compiler/src/Coln/Core/Layout.hs     |  4 ++--
 packages/coln-compiler/src/Coln/Core/Params.hs     | 14 +++++++-------
 .../src/Coln/Elaborator/Rules/Equality.hs          |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Layout.hs b/packages/coln-compiler/src/Coln/Core/Layout.hs
index b28f5478..c9ac08df 100644
--- a/packages/coln-compiler/src/Coln/Core/Layout.hs
+++ b/packages/coln-compiler/src/Coln/Core/Layout.hs
@@ -49,7 +49,7 @@ bind sc x a =
 
 layout :: Path -> Scope -> V.Ty N -> (Trie Generator, M.El N)
 layout p sc a
-  | (levelOf a).sort == Theory = case V.behavior a of
+  | (levelOf a).mlevel == Theory = case V.behavior a of
       V.LikeFunction ft -> do
         let x = argName sc.usedNames ft.cod
         let (v, sc') = bind sc x ft.dom
@@ -71,7 +71,7 @@ layout p sc a
         (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"
-  | (levelOf a).sort == Set = do
+  | (levelOf a).mlevel == Set = do
       let gt = Leaf (Fun (toList sc.names) (toList sc.ctx) (readb sc.len a))
       let v = V.Lookup (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
       (gt, M.fromVEl sc.len v)
diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 1dea486b..9a782ddd 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -12,16 +12,16 @@ import Prettyprinter
 -- Level stuff (levels, universes, function variants)
 --------------------------------------------------------------------------------
 
-data Sort
+data MLevel
   = Set
   | Theory
   | Top
   deriving (Eq, Show)
 
-instance DPretty Sort where
+instance DPretty MLevel where
   dpretty = pretty . show
 
-instance PartialOrd Sort where
+instance PartialOrd MLevel where
   leq l1 l2 = case (l1, l2) of
     (Set, _) -> True
     (Theory, Set) -> False
@@ -29,8 +29,8 @@ instance PartialOrd Sort where
     (Top, Top) -> True
     (Top, _) -> False
 
-maxSort :: Sort -> Sort -> Sort
-maxSort l1 l2
+maxMLevel :: MLevel -> MLevel -> MLevel
+maxMLevel l1 l2
   | leq l1 l2 = l2
   | otherwise = l1
 
@@ -46,7 +46,7 @@ instance PartialOrd HLevel where
     (HSet, _) -> True
 
 data Level = Level {
-  sort :: Sort,
+  mlevel :: MLevel,
   hlevel :: HLevel }
   deriving (Eq, Show)
 
@@ -115,7 +115,7 @@ instance LevelOf FunctionVariant where
 class HasCodomain a b | a -> b where
   codOf :: a -> b
 
-instance HasCodomain FunctionVariant Sort where
+instance HasCodomain FunctionVariant MLevel where
   codOf = \case
     SetPropTheory -> Theory
     SetTheory -> Theory
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
index c96156cb..42a8e57f 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
@@ -28,7 +28,7 @@ formation sp lhs rhs = Typ \e -> do
       let msg = "types" <+> prtIn e lty <+> "and" <+> prtIn e rty <+> "of compared terms differ"
       let note = Just $ dpretty err
       failWithNote e.diagEnv sp TypeMismatch msg note
-    Right _ -> case (levelOf lty).sort of
+    Right _ -> case (levelOf lty).mlevel of
       Set -> pure $ equality $ S.EqualityType (fromVTy e.scope.len lty) elhs erhs
       _ -> do
         let msg = "equality requires data types, but" <+> prtIn e lty <+> "is a schema-level type"

From 48adbe8c58884a85c9238aac47ccb110bafe4e2e Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 12:45:52 +0100
Subject: [PATCH 03/11] Properly promote HLevel of equality type

---
 packages/coln-compiler/src/Coln/Core/Params.hs | 5 +++++
 packages/coln-compiler/src/Coln/Core/Value.hs  | 2 +-
 packages/coln-compiler/test/hlevel.glog        | 2 ++
 packages/coln-compiler/test/hlevel.output      | 4 ++++
 4 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 9a782ddd..2056d815 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -45,6 +45,11 @@ instance PartialOrd HLevel where
     (HSet, HProp) -> False
     (HSet, _) -> True
 
+equalityHLevelOf :: HLevel -> HLevel
+equalityHLevelOf = \case
+  HProp -> HProp
+  HSet -> HProp
+
 data Level = Level {
   mlevel :: MLevel,
   hlevel :: HLevel }
diff --git a/packages/coln-compiler/src/Coln/Core/Value.hs b/packages/coln-compiler/src/Coln/Core/Value.hs
index 929251cc..aa6e944b 100644
--- a/packages/coln-compiler/src/Coln/Core/Value.hs
+++ b/packages/coln-compiler/src/Coln/Core/Value.hs
@@ -225,7 +225,7 @@ instance LevelOf (Ty c) where
     Decode n -> decodesInto n.universe
     Function ft -> levelOf ft.variant
     Record rt -> rt.level
-    Eq ety -> levelOf ety.at
+    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
 
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.glog
index 18923b34..b092fb65 100644
--- a/packages/coln-compiler/test/hlevel.glog
+++ b/packages/coln-compiler/test/hlevel.glog
@@ -16,4 +16,6 @@ theory Q (F : Family) := sig
 
   showtype F.is-parent
   showtype F.is-parent father son
+
+  showtype son = father
 end
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
index 626081da..8ecf5c69 100644
--- a/packages/coln-compiler/test/hlevel.output
+++ b/packages/coln-compiler/test/hlevel.output
@@ -38,3 +38,7 @@ debug[D0315]: value F.is-parent has type F.person -> F.person -> Prop
 debug[D0315]: value F.is-parent father son has type Prop
 18 |   showtype F.is-parent father son
 18 |            ^^^^^^^^^^^^^^^^^^^^^^
+
+debug[D0315]: value son = father has type Prop
+20 |   showtype son = father
+20 |            ^^^^^^^^^^^^

From 5097fdc216ccafe709d2e759d41acd646e2d3444 Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 13:26:36 +0100
Subject: [PATCH 04/11] Add HUnit and HTop to HLevel

---
 .../coln-compiler/src/Coln/Core/Params.hs     | 21 +++++-----
 .../src/Coln/Elaborator/Rules/Function.hs     |  6 +--
 .../src/Coln/Elaborator/Rules/Record.hs       |  2 +-
 packages/coln-compiler/test/hlevel.glog       | 25 +++++++++++-
 packages/coln-compiler/test/hlevel.output     | 39 +++++++++++++++++--
 5 files changed, 74 insertions(+), 19 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 2056d815..3f448e4f 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -35,20 +35,21 @@ maxMLevel l1 l2
   | otherwise = l1
 
 data HLevel
-  = HProp
+  = HUnit
+  | HProp
   | HSet
-  deriving (Eq, Show)
+  | HTop
+  deriving (Eq, Show, Ord)
 
 instance PartialOrd HLevel where
-  leq l1 l2 = case (l1, l2) of
-    (HProp, _) -> True
-    (HSet, HProp) -> False
-    (HSet, _) -> True
+  leq l1 l2 = l1 <= l2
 
 equalityHLevelOf :: HLevel -> HLevel
 equalityHLevelOf = \case
-  HProp -> HProp
+  HUnit -> HUnit
+  HProp -> HUnit
   HSet -> HProp
+  HTop -> HTop
 
 data Level = Level {
   mlevel :: MLevel,
@@ -96,11 +97,11 @@ instance Pretty Universe where
 
 universeFor :: Level -> Maybe Universe
 universeFor = \case
-  Level Set HProp -> Just PropU
+  Level Set (HUnit; HProp) -> Just PropU
   Level Set HSet -> Just SetU
-  Level Theory HProp -> Just PropTheoryU
+  Level Theory (HUnit; HProp) -> Just PropTheoryU
   Level Theory HSet -> Just TheoryU
-  Level Top _ -> Nothing
+  Level _ _ -> Nothing
 
 data FunctionVariant
   = SetPropTheory -- TODO: better name?
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
index a7f35ba5..c454fcd9 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
@@ -17,10 +17,8 @@ import Coln.Report
 
 variantFor :: Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
 variantFor dom cod sp e = case (levelOf dom, levelOf cod) of
-  (Level Set _, Level Set HProp) -> pure SetPropTheory
-  (Level Set _, Level Theory HProp) -> pure SetPropTheory
-  (Level Set _, Level Set HSet) -> pure SetTheory
-  (Level Set _, Level Theory HSet) -> pure SetTheory
+  (Level Set _, Level (Set; Theory) (HUnit; HProp)) -> pure SetPropTheory
+  (Level Set _, Level (Set; Theory) (HSet; HTop)) -> pure SetTheory
   (Level Set _, Level Top _) -> pure TheoryTop
   (Level Theory _, Level _ _) -> pure TheoryTop
   (Level Top _, _) -> do
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
index 66a27695..8eeb3550 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
@@ -27,7 +27,7 @@ data FieldDeclaration
 
 formation :: [FieldDeclaration] -> Typ D
 formation fieldTyps = Typ $ \e -> do
-  let go _ [] = pure (Level Set HProp, [])
+  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
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.glog
index b092fb65..0a741e68 100644
--- a/packages/coln-compiler/test/hlevel.glog
+++ b/packages/coln-compiler/test/hlevel.glog
@@ -16,6 +16,29 @@ theory Q (F : Family) := sig
 
   showtype F.is-parent
   showtype F.is-parent father son
+end
+
+# Family analogies getting a bit risky
+theory HP := sig
+  person : Set
+
+  voldemort : person
+  tomriddle : person
+
+  showtype voldemort = tomriddle
+
+  reveal : voldemort = tomriddle
+
+  showtype reveal
+  showtype (reveal = reveal)
+end
+
+def Unit : Prop := sig
+end
+
+theory P := sig
+  showtype Unit
 
-  showtype son = father
+  u : Unit
+  showtype u = u
 end
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
index 8ecf5c69..4c52bb58 100644
--- a/packages/coln-compiler/test/hlevel.output
+++ b/packages/coln-compiler/test/hlevel.output
@@ -12,6 +12,23 @@ value: F => sig
   son : F.person
   father : F.person
 end
+global entry named HP
+type: Theory
+value: sig
+  person : Set
+  voldemort : person
+  tomriddle : person
+  reveal : voldemort = tomriddle
+end
+global entry named Unit
+type: Prop
+value: sig
+end
+global entry named P
+type: Theory
+value: sig
+  u : Unit
+end
 
 -- messages
 
@@ -39,6 +56,22 @@ debug[D0315]: value F.is-parent father son has type Prop
 18 |   showtype F.is-parent father son
 18 |            ^^^^^^^^^^^^^^^^^^^^^^
 
-debug[D0315]: value son = father has type Prop
-20 |   showtype son = father
-20 |            ^^^^^^^^^^^^
+debug[D0315]: value voldemort = tomriddle has type Prop
+28 |   showtype voldemort = tomriddle
+28 |            ^^^^^^^^^^^^^^^^^^^^^
+
+debug[D0315]: value reveal has type voldemort = tomriddle
+32 |   showtype reveal
+32 |            ^^^^^^
+
+debug[D0315]: value reveal = reveal has type Prop
+33 |   showtype (reveal = reveal)
+33 |             ^^^^^^^^^^^^^^^
+
+debug[D0315]: value Unit has type Prop
+40 |   showtype Unit
+40 |            ^^^^
+
+debug[D0315]: value u = u has type Prop
+43 |   showtype u = u
+43 |            ^^^^^

From aa4e5214e884cda22dd4aa0f78ee4df31e65e3f2 Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 14:46:18 +0100
Subject: [PATCH 05/11] Add `showlevel` debug command

---
 .../src/Coln/Elaborator/Debug.hs              |  4 ++
 .../coln-compiler/src/Coln/Frontend/Driver.hs |  5 +-
 .../src/Coln/Frontend/Notation.hs             |  1 +
 packages/coln-compiler/test/hlevel.glog       |  7 ++-
 packages/coln-compiler/test/hlevel.output     | 56 +++++++++++--------
 5 files changed, 48 insertions(+), 25 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Elaborator/Debug.hs b/packages/coln-compiler/src/Coln/Elaborator/Debug.hs
index d1121c50..b53f2151 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Debug.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Debug.hs
@@ -22,6 +22,7 @@ import Coln.Report
 data DebugCommand
   = ShowType Span (Syn N)
   | ShowTypeBehavior Span (Syn N)
+  | ShowLevel Span (Typ N)
   | Expand Span (Syn N)
 
 runDebug :: ElabEnv N -> DebugCommand -> IO ()
@@ -31,6 +32,9 @@ runDebug e (ShowType sp s) = do
 runDebug e (ShowTypeBehavior sp s) = do
   (a, m) <- s.elab e
   report e.diagEnv sp DebugMisc ("value" <+> prtIn e m.val <+> "has type" <+> prtIn e a <+> "with behavior" <+> prtIn e (V.behavior a))
+runDebug e (ShowLevel sp s) = do
+  ty <- s.elab e
+  report e.diagEnv sp DebugMisc ("type" <+> prtIn e ty <+> "has level" <+> (pretty $ show $ levelOf ty))
 runDebug e (Expand sp s) = do
   (_, m) <- s.elab e
   report e.diagEnv sp DebugMisc ("expands to:" <+> prtIn e (canon m.val))
diff --git a/packages/coln-compiler/src/Coln/Frontend/Driver.hs b/packages/coln-compiler/src/Coln/Frontend/Driver.hs
index 044ad96f..44a6cf91 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Driver.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Driver.hs
@@ -80,8 +80,11 @@ 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 showtype" n
+  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
diff --git a/packages/coln-compiler/src/Coln/Frontend/Notation.hs b/packages/coln-compiler/src/Coln/Frontend/Notation.hs
index c2469bfb..a537adee 100644
--- a/packages/coln-compiler/src/Coln/Frontend/Notation.hs
+++ b/packages/coln-compiler/src/Coln/Frontend/Notation.hs
@@ -20,6 +20,7 @@ lexConfig =
     , ("import", K.Decl)
     , ("showtypeb", K.Decl)
     , ("showtype", K.Decl)
+    , ("showlevel", K.Decl)
     , ("expand", K.Decl)
     , ("end", K.End)
     , ("Set", K.AKeyword)
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.glog
index 0a741e68..80241cfa 100644
--- a/packages/coln-compiler/test/hlevel.glog
+++ b/packages/coln-compiler/test/hlevel.glog
@@ -5,6 +5,7 @@ theory Family := sig
   happy : Prop
 
   showtype happy
+  showlevel happy
   showtype is-parent
   showtype happy -> person
   showtype person -> happy
@@ -25,12 +26,12 @@ theory HP := sig
   voldemort : person
   tomriddle : person
 
-  showtype voldemort = tomriddle
+  showlevel voldemort = tomriddle
 
   reveal : voldemort = tomriddle
 
   showtype reveal
-  showtype (reveal = reveal)
+  showlevel (reveal = reveal)
 end
 
 def Unit : Prop := sig
@@ -38,7 +39,9 @@ end
 
 theory P := sig
   showtype Unit
+  showlevel Unit
 
   u : Unit
   showtype u = u
+  showlevel u = u
 end
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
index 4c52bb58..11c83148 100644
--- a/packages/coln-compiler/test/hlevel.output
+++ b/packages/coln-compiler/test/hlevel.output
@@ -36,42 +36,54 @@ debug[D0315]: value happy has type Prop
 7 |   showtype happy
 7 |            ^^^^^
 
+debug[D0315]: type happy has level Level {mlevel = Set, hlevel = HProp}
+8 |   showlevel happy
+8 |             ^^^^^
+
 debug[D0315]: value is-parent has type person -> person -> Prop
-8 |   showtype is-parent
-8 |            ^^^^^^^^^
+9 |   showtype is-parent
+9 |            ^^^^^^^^^
 
 debug[D0315]: value happy -> person has type Theory
-9 |   showtype happy -> person
-9 |            ^^^^^^^^^^^^^^^
+10 |   showtype happy -> person
+10 |            ^^^^^^^^^^^^^^^
 
 debug[D0315]: value person -> happy has type PropTheory
-10 |   showtype person -> happy
-10 |            ^^^^^^^^^^^^^^^
+11 |   showtype person -> happy
+11 |            ^^^^^^^^^^^^^^^
 
 debug[D0315]: value F.is-parent has type F.person -> F.person -> Prop
-17 |   showtype F.is-parent
-17 |            ^^^^^^^^^^^
+18 |   showtype F.is-parent
+18 |            ^^^^^^^^^^^
 
 debug[D0315]: value F.is-parent father son has type Prop
-18 |   showtype F.is-parent father son
-18 |            ^^^^^^^^^^^^^^^^^^^^^^
+19 |   showtype F.is-parent father son
+19 |            ^^^^^^^^^^^^^^^^^^^^^^
 
-debug[D0315]: value voldemort = tomriddle has type Prop
-28 |   showtype voldemort = tomriddle
-28 |            ^^^^^^^^^^^^^^^^^^^^^
+debug[D0315]: type voldemort = tomriddle has level Level {mlevel = Set, hlevel = HProp}
+29 |   showlevel voldemort = tomriddle
+29 |             ^^^^^^^^^^^^^^^^^^^^^
 
 debug[D0315]: value reveal has type voldemort = tomriddle
-32 |   showtype reveal
-32 |            ^^^^^^
+33 |   showtype reveal
+33 |            ^^^^^^
 
-debug[D0315]: value reveal = reveal has type Prop
-33 |   showtype (reveal = reveal)
-33 |             ^^^^^^^^^^^^^^^
+debug[D0315]: type reveal = reveal has level Level {mlevel = Set, hlevel = HUnit}
+34 |   showlevel (reveal = reveal)
+34 |              ^^^^^^^^^^^^^^^
 
 debug[D0315]: value Unit has type Prop
-40 |   showtype Unit
-40 |            ^^^^
+41 |   showtype Unit
+41 |            ^^^^
+
+debug[D0315]: type Unit has level Level {mlevel = Set, hlevel = HProp}
+42 |   showlevel Unit
+42 |             ^^^^
 
 debug[D0315]: value u = u has type Prop
-43 |   showtype u = u
-43 |            ^^^^^
+45 |   showtype u = u
+45 |            ^^^^^
+
+debug[D0315]: type u = u has level Level {mlevel = Set, hlevel = HUnit}
+46 |   showlevel u = u
+46 |             ^^^^^

From 2f6f896dcb3ee33e4c1d3b611818b1a82e39c2cd Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 15:15:21 +0100
Subject: [PATCH 06/11] maxLevel should be componentwise

---
 packages/coln-compiler/src/Coln/Core/Params.hs |  4 +---
 packages/coln-compiler/test/hlevel.glog        |  5 +++++
 packages/coln-compiler/test/hlevel.output      | 13 +++++++++++++
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 3f448e4f..672adea8 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -60,9 +60,7 @@ instance PartialOrd Level where
   leq (Level s1 h1) (Level s2 h2) = s1 `leq` s2 && h1 `leq` h2
 
 maxLevel :: Level -> Level -> Level
-maxLevel l1 l2
-  | leq l1 l2 = l2
-  | otherwise = l1
+maxLevel l1 l2 = Level (maxMLevel l1.mlevel l2.mlevel) (max l1.hlevel l2.hlevel)
 
 class LevelOf a where
   levelOf :: a -> Level
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.glog
index 80241cfa..011b1346 100644
--- a/packages/coln-compiler/test/hlevel.glog
+++ b/packages/coln-compiler/test/hlevel.glog
@@ -45,3 +45,8 @@ theory P := sig
   showtype u = u
   showlevel u = u
 end
+
+def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
+  f : A -> P
+  a : A
+end
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
index 11c83148..4234eadc 100644
--- a/packages/coln-compiler/test/hlevel.output
+++ b/packages/coln-compiler/test/hlevel.output
@@ -87,3 +87,16 @@ debug[D0315]: value u = u has type Prop
 debug[D0315]: type u = u has level Level {mlevel = Set, hlevel = HUnit}
 46 |   showlevel u = u
 46 |             ^^^^^
+
+error[E0307]: type sig
+  f : A -> P
+  a : A
+end too large for universe Set
+49 | def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
+49 |                                                           ^^^
+50 |   f : A -> P
+50 | ^^^^^^^^^^^^
+51 |   a : A
+51 | ^^^^^^^
+52 | end
+52 | ^^^

From 8959cfe155237e5218ff5c04f01357455ca037f9 Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Fri, 19 Jun 2026 19:35:25 +0100
Subject: [PATCH 07/11] Give FunctionVariant an HLevel instead of a separate
 constructor

---
 .../coln-compiler/src/Coln/Core/Params.hs     | 26 ++++++++++++-------
 .../src/Coln/Elaborator/Rules/Function.hs     | 14 +++++-----
 2 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 672adea8..8560fd84 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -101,27 +101,35 @@ universeFor = \case
   Level Theory HSet -> Just TheoryU
   Level _ _ -> Nothing
 
-data FunctionVariant
-  = SetPropTheory -- TODO: better name?
-  | SetTheory
+data FunctionVariantMLevel
+  = SetTheory
   | TheoryTop
   deriving (Eq, Show)
 
+functionMLevelFor :: MLevel -> MLevel -> Maybe FunctionVariantMLevel
+functionMLevelFor v1 v2 = case (v1, v2) of
+  (Set, (Set; Theory)) -> pure SetTheory
+  (Set, Top) -> pure TheoryTop
+  (Theory, _) -> pure TheoryTop
+  (Top, _) -> Nothing
+
+data FunctionVariant = FunctionVariant { mlevel :: FunctionVariantMLevel, hlevel :: HLevel }
+  deriving (Eq, Show)
+
 instance Pretty FunctionVariant where
   pretty = pretty . show
 
 instance LevelOf FunctionVariant where
-  levelOf = \case
-    SetPropTheory -> Level Theory HProp
-    SetTheory -> Level Theory HSet
-    TheoryTop -> Level Top HSet
+  levelOf v = Level mlevel v.hlevel
+    where mlevel = case v.mlevel of
+                     SetTheory -> Theory
+                     TheoryTop -> Top
 
 class HasCodomain a b | a -> b where
   codOf :: a -> b
 
 instance HasCodomain FunctionVariant MLevel where
-  codOf = \case
-    SetPropTheory -> Theory
+  codOf v = case v.mlevel of
     SetTheory -> Theory
     TheoryTop -> Top
 
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
index c454fcd9..cb268b18 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
@@ -16,14 +16,12 @@ import Coln.Elaborator.Judgment
 import Coln.Report
 
 variantFor :: Ty N -> Ty N -> Span -> ElabEnv c -> IO FunctionVariant
-variantFor dom cod sp e = case (levelOf dom, levelOf cod) of
-  (Level Set _, Level (Set; Theory) (HUnit; HProp)) -> pure SetPropTheory
-  (Level Set _, Level (Set; Theory) (HSet; HTop)) -> pure SetTheory
-  (Level Set _, Level Top _) -> pure TheoryTop
-  (Level Theory _, Level _ _) -> pure TheoryTop
-  (Level Top _, _) -> do
-    let msg = "higher-order theories are not supported"
-    failWith e.diagEnv sp FunctionDomainTooLarge msg
+variantFor dom cod sp e =
+  case functionMLevelFor (levelOf dom).mlevel (levelOf cod).mlevel of
+    Just l -> pure (FunctionVariant l (levelOf cod).hlevel)
+    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)
 

From 2ce5a8f84c28539a4aa86f0353c39f148cb38c56 Mon Sep 17 00:00:00 2001
From: Owen Lynch <root@owenlynch.org>
Date: Tue, 23 Jun 2026 17:06:23 +0100
Subject: [PATCH 08/11] formatting

---
 packages/coln-compiler/src/Coln/Core/Params.hs   | 16 +++++++++-------
 .../src/Coln/Elaborator/Rules/Record.hs          |  2 +-
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 8560fd84..c053b629 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -51,9 +51,10 @@ equalityHLevelOf = \case
   HSet -> HProp
   HTop -> HTop
 
-data Level = Level {
-  mlevel :: MLevel,
-  hlevel :: HLevel }
+data Level = Level
+  { mlevel :: MLevel
+  , hlevel :: HLevel
+  }
   deriving (Eq, Show)
 
 instance PartialOrd Level where
@@ -113,7 +114,7 @@ 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}
   deriving (Eq, Show)
 
 instance Pretty FunctionVariant where
@@ -121,9 +122,10 @@ instance Pretty FunctionVariant where
 
 instance LevelOf FunctionVariant where
   levelOf v = Level mlevel v.hlevel
-    where mlevel = case v.mlevel of
-                     SetTheory -> Theory
-                     TheoryTop -> Top
+   where
+    mlevel = case v.mlevel of
+      SetTheory -> Theory
+      TheoryTop -> Top
 
 class HasCodomain a b | a -> b where
   codOf :: a -> b
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
index 8eeb3550..3a2eeb5a 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
@@ -28,7 +28,7 @@ data FieldDeclaration
 formation :: [FieldDeclaration] -> Typ D
 formation fieldTyps = Typ $ \e -> do
   let go _ [] = pure (Level Set HUnit, [])
-      go e' ((FieldDeclaration x typ):rest) = do
+      go e' ((FieldDeclaration x typ) : rest) = do
         ty <- typ.elab e'
         (l, fieldTys) <- go (e'{scope = bind x ty.val e'.scope}) rest
         pure (maxLevel l (levelOf ty), (x, ty) : fieldTys)

From a38bec45a90ece4bbf7d31857170f723e42ecb7b Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Wed, 24 Jun 2026 15:57:10 +0100
Subject: [PATCH 09/11] Punt on `layout` for `Prop`, for now

---
 packages/coln-compiler/src/Coln/Core/Layout.hs | 3 ++-
 packages/coln-compiler/test/paths.output       | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Layout.hs b/packages/coln-compiler/src/Coln/Core/Layout.hs
index c9ac08df..49cd53d1 100644
--- a/packages/coln-compiler/src/Coln/Core/Layout.hs
+++ b/packages/coln-compiler/src/Coln/Core/Layout.hs
@@ -65,7 +65,8 @@ layout p sc a
         let (gts, ms) = go rt.capture (toList rt.fieldTypes)
         let m = M.cons (Dict rt.fieldTypes.head (Vector.fromList ms))
         (Node $ Dict rt.fieldTypes.head (Vector.fromList gts), m)
-      V.LikeU SetU -> do
+      V.LikeU (SetU; PropU) -> do
+        -- TODO: layout Prop correctly
         let gt = Leaf (Rel (toList sc.names) (toList sc.ctx))
         let a = V.EltOf (TableName sc.realm p) (fromList $ zip (toList sc.names) (toList sc.bound))
         (gt, M.code (M.fromVTy sc.len a))
diff --git a/packages/coln-compiler/test/paths.output b/packages/coln-compiler/test/paths.output
index ca1c9f77..a3ee8f95 100644
--- a/packages/coln-compiler/test/paths.output
+++ b/packages/coln-compiler/test/paths.output
@@ -3,12 +3,12 @@ global entry named Graph
 type: Theory
 value: sig
   V : Set
-  E : V -> V -> Set
+  E : V -> V -> Prop
 end
 global entry named Reachability/motive
 type: (G : Graph) -> Theory
 value: G => sig
-  t : G.V -> G.V -> Set
+  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

From 59815a9cf89ad15545e85825aac98e0f5e4999eb Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Thu, 25 Jun 2026 12:07:22 +0100
Subject: [PATCH 10/11] Kill `PropTheory`

---
 packages/coln-compiler/src/Coln/Core/Params.hs | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index c053b629..1650a465 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -70,14 +70,12 @@ data Universe
   = PropU
   | SetU
   | TheoryU
-  | PropTheoryU -- TODO: better name?
   deriving (Eq, Show)
 
 decodesInto :: Universe -> Level
 decodesInto = \case
   PropU -> Level Set HProp
   SetU -> Level Set HSet
-  PropTheoryU -> Level Theory HProp
   TheoryU -> Level Theory HSet
 
 codesInto :: Universe -> Level
@@ -85,20 +83,17 @@ codesInto = \case
   PropU -> Level Theory HSet
   SetU -> Level Theory HSet
   TheoryU -> Level Top HSet
-  PropTheoryU -> Level Top HSet
 
 instance Pretty Universe where
   pretty = \case
     PropU -> "Prop"
     SetU -> "Set"
     TheoryU -> "Theory"
-    PropTheoryU -> "PropTheory"
 
 universeFor :: Level -> Maybe Universe
 universeFor = \case
   Level Set (HUnit; HProp) -> Just PropU
   Level Set HSet -> Just SetU
-  Level Theory (HUnit; HProp) -> Just PropTheoryU
   Level Theory HSet -> Just TheoryU
   Level _ _ -> Nothing
 

From 065385bf1f7c6b208c717b58106a3af4766588c6 Mon Sep 17 00:00:00 2001
From: mvr <mitchell.v.riley@gmail.com>
Date: Thu, 25 Jun 2026 12:41:58 +0100
Subject: [PATCH 11/11] `hlevel.glog` -> `hlevel.coln`, put former PropTheory
 into Theory

---
 .../coln-compiler/src/Coln/Core/Params.hs     |  2 +-
 .../test/{hlevel.glog => hlevel.coln}         |  2 +
 packages/coln-compiler/test/hlevel.output     | 66 +++++++++++--------
 3 files changed, 40 insertions(+), 30 deletions(-)
 rename packages/coln-compiler/test/{hlevel.glog => hlevel.coln} (93%)

diff --git a/packages/coln-compiler/src/Coln/Core/Params.hs b/packages/coln-compiler/src/Coln/Core/Params.hs
index 1650a465..808c4564 100644
--- a/packages/coln-compiler/src/Coln/Core/Params.hs
+++ b/packages/coln-compiler/src/Coln/Core/Params.hs
@@ -94,7 +94,7 @@ universeFor :: Level -> Maybe Universe
 universeFor = \case
   Level Set (HUnit; HProp) -> Just PropU
   Level Set HSet -> Just SetU
-  Level Theory HSet -> Just TheoryU
+  Level Theory (HSet; HProp) -> Just TheoryU
   Level _ _ -> Nothing
 
 data FunctionVariantMLevel
diff --git a/packages/coln-compiler/test/hlevel.glog b/packages/coln-compiler/test/hlevel.coln
similarity index 93%
rename from packages/coln-compiler/test/hlevel.glog
rename to packages/coln-compiler/test/hlevel.coln
index 011b1346..8006af7d 100644
--- a/packages/coln-compiler/test/hlevel.glog
+++ b/packages/coln-compiler/test/hlevel.coln
@@ -8,7 +8,9 @@ theory Family := sig
   showlevel happy
   showtype is-parent
   showtype happy -> person
+  showlevel happy -> person
   showtype person -> happy
+  showlevel person -> happy
 end
 
 theory Q (F : Family) := sig
diff --git a/packages/coln-compiler/test/hlevel.output b/packages/coln-compiler/test/hlevel.output
index 4234eadc..9325a41b 100644
--- a/packages/coln-compiler/test/hlevel.output
+++ b/packages/coln-compiler/test/hlevel.output
@@ -48,55 +48,63 @@ debug[D0315]: value happy -> person has type Theory
 10 |   showtype happy -> person
 10 |            ^^^^^^^^^^^^^^^
 
-debug[D0315]: value person -> happy has type PropTheory
-11 |   showtype person -> happy
-11 |            ^^^^^^^^^^^^^^^
+debug[D0315]: type happy -> person has level Level {mlevel = Theory, hlevel = HSet}
+11 |   showlevel happy -> person
+11 |             ^^^^^^^^^^^^^^^
+
+debug[D0315]: value person -> happy has type Theory
+12 |   showtype person -> happy
+12 |            ^^^^^^^^^^^^^^^
+
+debug[D0315]: type person -> happy has level Level {mlevel = Theory, hlevel = HProp}
+13 |   showlevel person -> happy
+13 |             ^^^^^^^^^^^^^^^
 
 debug[D0315]: value F.is-parent has type F.person -> F.person -> Prop
-18 |   showtype F.is-parent
-18 |            ^^^^^^^^^^^
+20 |   showtype F.is-parent
+20 |            ^^^^^^^^^^^
 
 debug[D0315]: value F.is-parent father son has type Prop
-19 |   showtype F.is-parent father son
-19 |            ^^^^^^^^^^^^^^^^^^^^^^
+21 |   showtype F.is-parent father son
+21 |            ^^^^^^^^^^^^^^^^^^^^^^
 
 debug[D0315]: type voldemort = tomriddle has level Level {mlevel = Set, hlevel = HProp}
-29 |   showlevel voldemort = tomriddle
-29 |             ^^^^^^^^^^^^^^^^^^^^^
+31 |   showlevel voldemort = tomriddle
+31 |             ^^^^^^^^^^^^^^^^^^^^^
 
 debug[D0315]: value reveal has type voldemort = tomriddle
-33 |   showtype reveal
-33 |            ^^^^^^
+35 |   showtype reveal
+35 |            ^^^^^^
 
 debug[D0315]: type reveal = reveal has level Level {mlevel = Set, hlevel = HUnit}
-34 |   showlevel (reveal = reveal)
-34 |              ^^^^^^^^^^^^^^^
+36 |   showlevel (reveal = reveal)
+36 |              ^^^^^^^^^^^^^^^
 
 debug[D0315]: value Unit has type Prop
-41 |   showtype Unit
-41 |            ^^^^
+43 |   showtype Unit
+43 |            ^^^^
 
 debug[D0315]: type Unit has level Level {mlevel = Set, hlevel = HProp}
-42 |   showlevel Unit
-42 |             ^^^^
+44 |   showlevel Unit
+44 |             ^^^^
 
 debug[D0315]: value u = u has type Prop
-45 |   showtype u = u
-45 |            ^^^^^
+47 |   showtype u = u
+47 |            ^^^^^
 
 debug[D0315]: type u = u has level Level {mlevel = Set, hlevel = HUnit}
-46 |   showlevel u = u
-46 |             ^^^^^
+48 |   showlevel u = u
+48 |             ^^^^^
 
 error[E0307]: type sig
   f : A -> P
   a : A
 end too large for universe Set
-49 | def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
-49 |                                                           ^^^
-50 |   f : A -> P
-50 | ^^^^^^^^^^^^
-51 |   a : A
-51 | ^^^^^^^
-52 | end
-52 | ^^^
+51 | def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
+51 |                                                           ^^^
+52 |   f : A -> P
+52 | ^^^^^^^^^^^^
+53 |   a : A
+53 | ^^^^^^^
+54 | end
+54 | ^^^