simple tests for univalence

diff --git a/examples/testUniv.ctt b/examples/testUniv.ctt
new file mode 100644 (file)
index 0000000..ecd0299
--- /dev/null
+++ b/examples/testUniv.ctt
@@ -0,0 +1,21 @@
+module testUniv where
+
+import testContr
+import testEquiv
+
+swap : bool -> bool = split
+ true -> false
+ false -> true
+
+lemSwap : (x:bool) -> Id bool (swap (swap x)) x = split
+ true -> <i>true
+ false -> <i>false
+
+isEquivSwap : isEquiv bool bool swap =
+ gradLemma bool bool swap swap lemSwap lemSwap
+
+eqBool : Id U bool bool = 
+ trans (equiv bool bool) (Id U bool bool) (<i>corrUniv bool bool@-i) (swap,isEquivSwap)
+
+test1 : bool = trans bool bool eqBool true
+test2 : bool = trans bool bool eqBool false