diff --git a/packages/coln-compiler/src/Coln/Core/Layout.hs b/packages/coln-compiler/src/Coln/Core/Layout.hs
index 853be9a..49cd53d 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).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
@@ -65,13 +65,14 @@ 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))
       V.NoRules -> panic "cannot layout type with no rules"
       V.LikeBuiltinTy _; V.LikeU _ -> panic "non-theory type"
-  | levelOf a == 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 dfbb03a..808c456 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 MLevel
   = Set
   | Theory
   | Top
   deriving (Eq, Show)
 
-instance DPretty Level where
+instance DPretty MLevel where
   dpretty = pretty . show
 
-instance PartialOrd Level where
+instance PartialOrd MLevel where
   leq l1 l2 = case (l1, l2) of
     (Set, _) -> True
     (Theory, Set) -> False
@@ -29,58 +29,104 @@ instance PartialOrd Level where
     (Top, Top) -> True
     (Top, _) -> False
 
-maxLevel :: Level -> Level -> Level
-maxLevel l1 l2
+maxMLevel :: MLevel -> MLevel -> MLevel
+maxMLevel l1 l2
   | leq l1 l2 = l2
   | otherwise = l1
 
+data HLevel
+  = HUnit
+  | HProp
+  | HSet
+  | HTop
+  deriving (Eq, Show, Ord)
+
+instance PartialOrd HLevel where
+  leq l1 l2 = l1 <= l2
+
+equalityHLevelOf :: HLevel -> HLevel
+equalityHLevelOf = \case
+  HUnit -> HUnit
+  HProp -> HUnit
+  HSet -> HProp
+  HTop -> HTop
+
+data Level = Level
+  { mlevel :: MLevel
+  , 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 = Level (maxMLevel l1.mlevel l2.mlevel) (max l1.hlevel l2.hlevel)
+
 class LevelOf a where
   levelOf :: a -> Level
 
 data Universe
-  = SetU
+  = PropU
+  | SetU
   | TheoryU
   deriving (Eq, Show)
 
 decodesInto :: Universe -> Level
 decodesInto = \case
-  SetU -> Set
-  TheoryU -> Theory
+  PropU -> Level Set HProp
+  SetU -> Level Set HSet
+  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
 
 instance Pretty Universe where
   pretty = \case
+    PropU -> "Prop"
     SetU -> "Set"
     TheoryU -> "Theory"
 
 universeFor :: Level -> Maybe Universe
 universeFor = \case
-  Set -> Just SetU
-  Theory -> Just TheoryU
-  Top -> Nothing
+  Level Set (HUnit; HProp) -> Just PropU
+  Level Set HSet -> Just SetU
+  Level Theory (HSet; HProp) -> Just TheoryU
+  Level _ _ -> Nothing
 
-data FunctionVariant
+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
-    SetTheory -> Theory
-    TheoryTop -> Top
+  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 Level where
-  codOf = \case
+instance HasCodomain FunctionVariant MLevel where
+  codOf v = case v.mlevel of
     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 8821d0f..0d2ef99 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 184fda9..aa6e944 100644
--- a/packages/coln-compiler/src/Coln/Core/Value.hs
+++ b/packages/coln-compiler/src/Coln/Core/Value.hs
@@ -225,9 +225,9 @@ instance LevelOf (Ty c) where
     Decode n -> decodesInto n.universe
     Function ft -> levelOf ft.variant
     Record rt -> rt.level
-    Eq ety -> levelOf ety.at
-    BuiltinTy _ -> Set
-    EltOf _ _ -> Set
+    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
 
 behavior :: Ty c -> TypeBehavior
 behavior = \case
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Debug.hs b/packages/coln-compiler/src/Coln/Elaborator/Debug.hs
index d1121c5..b53f215 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/Elaborator/Rules/Equality.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Equality.hs
index 8223601..42a8e57 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).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"
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
index 9fa495e..cb268b1 100644
--- a/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
+++ b/packages/coln-compiler/src/Coln/Elaborator/Rules/Function.hs
@@ -16,12 +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
-  ((Set, Set); (Set, Theory)) -> pure SetTheory
-  ((Set, Top); (Theory, _)) -> pure TheoryTop
-  (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)
 
diff --git a/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs b/packages/coln-compiler/src/Coln/Elaborator/Rules/Record.hs
index 5542b28..3a2eeb5 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 (Set, [])
+  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/src/Coln/Frontend/Driver.hs b/packages/coln-compiler/src/Coln/Frontend/Driver.hs
index 9d8e282..44a6cf9 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
@@ -194,7 +197,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/src/Coln/Frontend/Notation.hs b/packages/coln-compiler/src/Coln/Frontend/Notation.hs
index c2469bf..a537ade 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/ancestor.output b/packages/coln-compiler/test/ancestor.output
index d4b291f..8172067 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.coln b/packages/coln-compiler/test/hlevel.coln
new file mode 100644
index 0000000..8006af7
--- /dev/null
+++ b/packages/coln-compiler/test/hlevel.coln
@@ -0,0 +1,54 @@
+theory Family := sig
+  person : Set
+  is-parent : person -> person -> Prop
+
+  happy : Prop
+
+  showtype happy
+  showlevel happy
+  showtype is-parent
+  showtype happy -> person
+  showlevel happy -> person
+  showtype person -> happy
+  showlevel 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
+
+# Family analogies getting a bit risky
+theory HP := sig
+  person : Set
+
+  voldemort : person
+  tomriddle : person
+
+  showlevel voldemort = tomriddle
+
+  reveal : voldemort = tomriddle
+
+  showtype reveal
+  showlevel (reveal = reveal)
+end
+
+def Unit : Prop := sig
+end
+
+theory P := sig
+  showtype Unit
+  showlevel Unit
+
+  u : Unit
+  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
new file mode 100644
index 0000000..9325a41
--- /dev/null
+++ b/packages/coln-compiler/test/hlevel.output
@@ -0,0 +1,110 @@
+-- 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
+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
+
+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
+9 |   showtype is-parent
+9 |            ^^^^^^^^^
+
+debug[D0315]: value happy -> person has type Theory
+10 |   showtype happy -> person
+10 |            ^^^^^^^^^^^^^^^
+
+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
+20 |   showtype F.is-parent
+20 |            ^^^^^^^^^^^
+
+debug[D0315]: value F.is-parent father son has type Prop
+21 |   showtype F.is-parent father son
+21 |            ^^^^^^^^^^^^^^^^^^^^^^
+
+debug[D0315]: type voldemort = tomriddle has level Level {mlevel = Set, hlevel = HProp}
+31 |   showlevel voldemort = tomriddle
+31 |             ^^^^^^^^^^^^^^^^^^^^^
+
+debug[D0315]: value reveal has type voldemort = tomriddle
+35 |   showtype reveal
+35 |            ^^^^^^
+
+debug[D0315]: type reveal = reveal has level Level {mlevel = Set, hlevel = HUnit}
+36 |   showlevel (reveal = reveal)
+36 |              ^^^^^^^^^^^^^^^
+
+debug[D0315]: value Unit has type Prop
+43 |   showtype Unit
+43 |            ^^^^
+
+debug[D0315]: type Unit has level Level {mlevel = Set, hlevel = HProp}
+44 |   showlevel Unit
+44 |             ^^^^
+
+debug[D0315]: value u = u has type Prop
+47 |   showtype u = u
+47 |            ^^^^^
+
+debug[D0315]: type u = u has level Level {mlevel = Set, hlevel = HUnit}
+48 |   showlevel u = u
+48 |             ^^^^^
+
+error[E0307]: type sig
+  f : A -> P
+  a : A
+end too large for universe Set
+51 | def LevelJoinRecordIsNotSet (A : Set) (P : Prop) : Set := sig
+51 |                                                           ^^^
+52 |   f : A -> P
+52 | ^^^^^^^^^^^^
+53 |   a : A
+53 | ^^^^^^^
+54 | end
+54 | ^^^
diff --git a/packages/coln-compiler/test/paths.output b/packages/coln-compiler/test/paths.output
index ca1c9f7..a3ee8f9 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