From b415b803449a44ddfef3b35e22076a321d15bc70 Mon Sep 17 00:00:00 2001
From: coquand <coquand@chalmers.se>
Date: Wed, 29 Apr 2015 12:28:10 +0200
Subject: [PATCH] added hopf fibration

---
 examples/hopf.ctt | 10 ++++++++++
 examples/mult.ctt |  9 ++++++---
 2 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 examples/hopf.ctt

diff --git a/examples/hopf.ctt b/examples/hopf.ctt
new file mode 100644
index 0000000..b4a02f4
--- /dev/null
+++ b/examples/hopf.ctt
@@ -0,0 +1,10 @@
+module hopf where
+
+import truncS2
+import mult
+
+hopf : S2 -> U = split
+ north -> S1
+ south -> S1
+ merid x @ i -> eqS1 x @ i
+
diff --git a/examples/mult.ctt b/examples/mult.ctt
index d6f0f37..a0a88cf 100644
--- a/examples/mult.ctt
+++ b/examples/mult.ctt
@@ -9,21 +9,24 @@ invS : S1 -> S1 = split
  base -> base
  loop @ i -> loop1 @ -i
 
+
+
 lemInv : (x:S1) -> Id S1 (mult x (invS x)) base = split 
  base -> refl S1 base
- loop @ i -> <j> loop1 @i\/-i\/j
+ loop @ i -> <j>base
 
 test0S : Z = winding (<i>mult (loop2@i) (invS (loop2@i)))
+loop4 : loopS1 = compS1 loop2 loop2
 test00S : Z = winding (<i>mult (loop4@i) (invS (loop4@i)))
 
 lemInv1 : (x:S1) -> Id S1 (mult (invS x) x) base = split
  base -> refl S1 base
- loop @ i -> <j> loop1 @ -i\/i\/j
+ loop @ i -> <j> base -- loop1 @ -i\/i\/j
 
 test : loopS1 = <i> mult (loop1@i) (loop1@-i)
 test1 : IdP (<i>Id S1 (mult (loop1@i) base) (mult (loop1@i) base)) loop1 loop1 = <i j> mult (loop1@i) (loop1@j)
 test2 : loopS1 = <i> mult (loop1@i) (loop1@i)
-test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2
+-- test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2
 
 lemBase (y:S1) : Id S1 (mult base (mult base y)) y = 
  compId S1 (mult base (mult base y)) (mult base y) y (idL (mult base y)) (idL y)
-- 
2.34.1