...

[bitonic-mengthesis.git] / itt.ka

diff --git a/itt.ka b/itt.ka
new file mode 100644 (file)
index 0000000..e9decf6
--- /dev/null
+++ b/itt.ka
@@ -0,0 +1,17 @@
+data Empty : * => { }
+
+absurd [A : *] [x : Empty] : A => (
+  Empty-Elim x (\_ => A)
+)
+
+neg [A : *] : * => (A -> Empty)
+
+record Unit : * => tt { }
+
+record Prod : [A : *] [B : A -> *] -> * =>
+  prod {fst : A, snd : B fst}
+
+data Bool : * => { true : Bool | false : Bool }
+
+-- The if_then_else_ is provided by Bool-Elim
+