One/Unit

2 files changed, 7 insertions, 2 deletions

diff --git a/app/Main.hs b/app/Main.hs
index f8b586a..4c0014e 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -18,6 +18,8 @@ main = do
 
   let env0 = Map.fromList
         [("Level", Nothing :| TLevelUniv)
+        ,("One", Nothing :| TSet TIZero)
+        ,("Unit", Nothing :| TOne)
         ,("lzero", Nothing :| TLevel)
         ,("lsuc", Nothing :| TPi "x" TLevel TLevel)]
 
diff --git a/example.txt b/example.txt
index 1d96c5f..29ab618 100644
--- a/example.txt
+++ b/example.txt
@@ -1,2 +1,5 @@
-foo : (l : Level) -> (a : Set l) -> (x : a) -> a
-foo = \(l : Level) -> \(a : Set l) -> \(x : a) -> x
+id : (l : Level) -> (a : Set l) -> (x : a) -> a
+id = \(l : Level) -> \(a : Set l) -> \(x : a) -> x
+
+unitfoo : (_ : One) -> One
+unitfoo = \(Unit : One) -> Unit