From cf484ebee67f773b3cef8ccaab361d773016a711 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 4 Jan 2016 19:47:44 +0100
Subject: [PATCH] Add bool example to univalence.ctt

---
 examples/testUniv.ctt   | 21 ---------------------
 examples/univalence.ctt | 15 +++++++++++++++
 2 files changed, 15 insertions(+), 21 deletions(-)
 delete mode 100644 examples/testUniv.ctt

diff --git a/examples/testUniv.ctt b/examples/testUniv.ctt
deleted file mode 100644
index 8662cda..0000000
--- a/examples/testUniv.ctt
+++ /dev/null
@@ -1,21 +0,0 @@
-module testUniv where
-
-import testContr
-import equiv
-
-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
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 513591a..d62066b 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -139,6 +139,9 @@ corrUniv (A X:U) : Id U (Id U X A) (equiv X A) =
 
 corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A)
 
+
+-- Some tests of normal forms:
+
 testUniv1 (A:U) : Id U A A =
   trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
 
@@ -158,6 +161,18 @@ ntestUniv2 : bool =
   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
 
 
+-- A small test of univalence using boolean negation
+isEquivNegBool : isEquiv bool bool negBool =
+ gradLemma bool bool negBool negBool negBoolK negBoolK
+
+eqBool : Id U bool bool = 
+ trans (equiv bool bool) (Id U bool bool)
+       (<i> corrUniv bool bool @ -i) (negBool,isEquivNegBool)
+
+test1 : bool = trans bool bool eqBool true
+test2 : bool = trans bool bool eqBool false
+
+
 ------------------------------------------------------------------------------
 -- The direct proof of univalence using transEquiv:
 
-- 
2.34.1