From 3d2a7d4bee17a1a652ac05b6087b9d2c1761699a Mon Sep 17 00:00:00 2001
From: coquand <coquand@chalmers.se>
Date: Sun, 27 Dec 2015 10:09:05 +0100
Subject: [PATCH] simple tests for univalence

---
 examples/testUniv.ctt | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 examples/testUniv.ctt

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
-- 
2.34.1