From: coquand <coquand@chalmers.se>
Date: Sun, 27 Dec 2015 09:09:05 +0000 (+0100)
Subject: simple tests for univalence
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=3d2a7d4bee17a1a652ac05b6087b9d2c1761699a;p=cubicaltt.git

simple tests for univalence
---

diff --git a/examples/testUniv.ctt b/examples/testUniv.ctt
new file mode 100644
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