From: Anders <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 14:39:28 +0000 (+0200)
Subject: Lots of cleaning in the examples
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4ccf678a4ede6c4d307738faac7b17b26eb319cc;p=cubicaltt.git

Lots of cleaning in the examples
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index dbbcab8..f94af65 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -4,18 +4,18 @@ import prelude
 
 data bool = false | true
 
-neg : bool -> bool = split
+negBool : bool -> bool = split
   false -> true
   true  -> false
 
-negK : (b : bool) -> Id bool (neg (neg b)) b = split
+negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split
   false -> refl bool false
   true -> refl bool true
 
-negEq : Id U bool bool =
-  <i> glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]
+negBoolEq : Id U bool bool =
+  <i> glue bool [ (i = 0) -> (bool,negBool,negBool,negBoolK,negBoolK) ]
 
-test : bool = transport negEq true
+test : bool = transport negBoolEq true
 
 data F2 = zeroF2 | oneF2
 
@@ -38,7 +38,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
 boolEqF2 : Id U bool F2 =
  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
   
-negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
+negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool
 
 lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
   J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A)
@@ -48,21 +48,21 @@ test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true
 
 F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2
 
-negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
+negBool' : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
 
 F2EqBoolComp : Id U F2 bool =
-  compId U F2 bool bool F2EqBool negEq
+  compId U F2 bool bool F2EqBool negBoolEq
 
 test2 : bool = transport F2EqBoolComp oneF2
 
 negNegEq : Id U bool bool =
-  compId U bool bool bool negEq negEq
+  compId U bool bool bool negBoolEq negBoolEq
 
 test3 : bool = transport negNegEq true
 test4 : Id U bool bool = <i> negNegEq @ i
 
 kanBool : Id U bool bool =
-  kan U bool bool bool bool negEq negEq negEq
+  kan U bool bool bool bool negBoolEq negBoolEq negBoolEq
 
 squareBoolF2 : Square U bool bool (refl U bool) bool F2
                   boolEqF2 (refl U bool)  boolEqF2 =
diff --git a/examples/circle.ctt b/examples/circle.ctt
index d7a0a17..758e412 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -1,34 +1,39 @@
 module circle where
 
 import bool
-import integer
+import int
 
-data S1 = base | loop @ base ~ base
+data S1 = base
+        | loop @ base ~ base
+
+loopS1 : U = Id S1 base base
+
+loop1 : Id S1 base base = <i> loop{S1} @ i
+
+invLoop : loopS1 = inv S1 base base loop1
 
 moebius : S1 -> U = split
   base -> bool
-  loop @ i -> negEq @ i
-
-loop' : Id S1 base base = <i> loop{S1} @ i
+  loop @ i -> negBoolEq @ i
 
 helix : S1 -> U = split
   base -> Z
   loop @ i -> sucIdZ @ i
 
-loopS1 : U = Id S1 base base 
-
 winding (p : loopS1) : Z = transport rem zeroZ
   where
     rem : Id U Z Z = <i> helix (p @ i)
 
+compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base
+
 -- All of these should be equal to "posZ (suc zero)":
-loop2 : loopS1 = compId S1 base base base loop' loop'
-loop2' : loopS1 = compId' S1 base base base loop' loop'
-loop2'' : loopS1 = compId'' S1 base base loop' base loop'
+loop2 : loopS1 = compS1 loop1 loop1
+loop2' : loopS1 = compId' S1 base base base loop1 loop1
+loop2'' : loopS1 = compId'' S1 base base loop1 base loop1
 
 mLoop : (x : S1) -> Id S1 x x = split
-  base -> loop'
-  loop @ i -> (constSquare S1 base loop') @ i
+  base -> loop1
+  loop @ i -> (constSquare S1 base loop1) @ i
 
 mult (x : S1) : S1 -> S1 = split
   base -> x
diff --git a/examples/discor.ctt b/examples/discor.ctt
index ecfc665..e983ff1 100644
--- a/examples/discor.ctt
+++ b/examples/discor.ctt
@@ -2,20 +2,6 @@ module discor where
 
 import prelude
 
-data or (A B:U) = inl (a:A) | inr (b:B)
-
-data Unit = tt
-
-data N0 = 
-
-efq (A:U) : N0 -> A = split{}
-
-neg (A:U) : U = A -> N0
-
-dec (A:U) : U = or A (neg A)
-
-discrete (A:U) : U = (a b:A) -> dec (Id A a b)
-
 inlNotinr (A B:U) (a:A) (b:B) (h: Id (or A B) (inl a) (inr b)) : N0 = 
  subst (or A B) T (inl a) (inr b) h tt
  where
@@ -30,8 +16,6 @@ inrNotinl (A B:U) (a:A) (b:B) (h : Id (or A B) (inr b) (inl a)) : N0 =
        inl _ -> N0
        inr _ -> Unit
 
-injective (A B:U) (f:A->B) : U = (a0 a1:A) -> Id B (f a0) (f a1) -> Id A a0 a1
-
 injInl (A B :U) (x0 x1:A) (h : Id (or A B) (inl x0) (inl x1)) : Id A x0 x1 = 
  subst (or A B) T (inl x0) (inl x1) h (refl A x0)
  where
@@ -46,7 +30,9 @@ injInr (A B :U) (x0 x1:B) (h: Id (or A B) (inr x0) (inr x1)) : Id B x0 x1 =
          inl _ -> N0
          inr x -> Id B x0 x
 
-orDisc (A B : U) (dA: discrete A) (dB: discrete B) : (z z1 : or A B) -> dec (Id (or A B) z z1) = split
+-- If A and B are discrete then "A or B" is discrete
+orDisc (A B : U) (dA : discrete A) (dB : discrete B) :
+  (z z1 : or A B) -> dec (Id (or A B) z z1) = split
   inl a -> rem1
     where rem1 : (z1:or A B) -> dec (Id (or A B) (inl a) z1) = split
             inl a1 -> rem (dA a a1)
diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 5e32517..d1d860a 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -2,8 +2,6 @@ module equiv where
 
 import prelude
 
-and (A B:U) :U = (_:A) * B
-
 contr (A:U) : U = (_:A) * prop A
 
 isContr (A : U) : U = and (prop A) A
diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index e1a60c6..9db5b1d 100644
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -1,8 +1,6 @@
 module hedberg where
 
-import bool
-import discor
-import int
+import prelude
 
 const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)
 
@@ -10,60 +8,34 @@ decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split
   inl a -> inl (f a)
   inr h -> inr (\ (b:B) -> h (g b))
 
-caseNat (A:U) (a0 aS : A) : nat -> A = split
- zero -> a0
- suc n -> aS
-
-caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) 
-            : (n:nat) -> P n = split
- zero -> a0
- suc n -> aS n
-
-znots (n : nat) : neg (Id nat zero (suc n)) =
- \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero
-
-snotz (n : nat) : neg (Id nat (suc n) zero) =
- \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h)
-
-natDec : (n m:nat) -> dec (Id nat n m) = split
- zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m))
- suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n))
-   (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))
-                 (sucInj n m) (natDec n m))
-
 exConst (A : U) : U = (f:A -> A) * const A f
 
 decConst (A : U) : dec A -> exConst A = split
   inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)
   inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))
 
-hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) : 
+hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :
   (b : A) (p : Id A a b) ->
-            Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) = 
-  J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p)) 
+            Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =
+  J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p))
     (refl (Id A a a) (f a a (refl A a)))
 
-hedberg (A : U) (h:discrete A) (a b :A) (p q:Id A a b) : Id (Id A a b) p q = 
-   lemSimpl A a a b r p q rem5
-  where
-    rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)
-
-    f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1
-
-    fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2
+hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) ->
+   let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)
 
-    r : Id A a a = f a a (refl A a)
+       f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1
 
-    rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p
+       fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2
 
-    rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q
+       r : Id A a a = f a a (refl A a)
 
-    rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q
+       rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p
 
-    rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) = 
-     compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)
-                (f a b q) rem2 rem3 rem4
+       rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q
 
-natSet : set nat = hedberg nat natDec
+       rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q
 
-ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
+       rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) =
+         compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)
+                  (f a b q) rem2 rem3 rem4
+  in lemSimpl A a a b r p q rem5
diff --git a/examples/helix.ctt b/examples/helix.ctt
index 4f5d750..df89a0b 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -4,19 +4,12 @@ import circle
 import hedberg
 import retract
 
-loop1 : loopS1 = loop'
-triv : loopS1 = <i>base
-
-compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base
-
 encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ
 
 itLoop : nat -> loopS1 = split
  zero -> triv
  suc n -> compS1 (itLoop n) loop1
 
-invLoop : loopS1 = inv S1 base base loop1
-
 itLoopNeg : nat -> loopS1 = split 
  zero -> invLoop
  suc n -> compS1 (itLoopNeg n) invLoop
@@ -28,12 +21,6 @@ loopIt : Z -> loopS1 = split
 lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) = 
  refl loopS1 (itLoop (suc n))
 
-lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =
- <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]
-
-lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p)  (refl A b) =
-  <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]
-
 lemItNeg : (n:nat) -> Id loopS1  (transport (<i>Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split
  zero ->  lemInv S1 base base loop1
  suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop
@@ -71,8 +58,6 @@ lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x =
  base -> bP
  loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i
 
--- other proof?
-
 helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet
  where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)
 
@@ -82,7 +67,6 @@ retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p
 setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet
 
 -- S1 is a groupoid
-
 isGroupoidS1 : groupoid S1 = lem
  where
   lem2 : (y : S1) -> set (Id S1 base y)
@@ -182,10 +166,3 @@ invLaw : (x y : S1) ->
                 (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))
 
   bP : P base base = refl (Id S1 base base) (refl S1 base)
-
-
--- homotopy
-
-aLoop : loopS1 = <i>loop{S1}@(i/\-i)
-
-test : Id loopS1 triv aLoop = <j i>loop{S1}@(j/\i/\-i)
diff --git a/examples/int.ctt b/examples/int.ctt
index 3ff9691..3d12f32 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -40,3 +40,5 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split
   inr v -> refl Z (inr v)
 
 sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
+
+ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
diff --git a/examples/interval.ctt b/examples/interval.ctt
index ee1f108..d5a2c43 100644
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -4,6 +4,7 @@ import prelude
 
 data I = zero | one | seg @ zero ~ one
 
+-- Proof of funext from the interval
 fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
      Id (A -> B) f g = <j> (\(x : A) -> htpy x (seg{I} @ j))
   where htpy (x : A) : I -> B = split
diff --git a/examples/nat.ctt b/examples/nat.ctt
index a3a7be4..f36e78d 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -1,6 +1,6 @@
 module nat where
 
-import prelude
+import hedberg
 
 data nat = zero | suc (n : nat)
 
@@ -31,3 +31,26 @@ test : Id (nat -> nat) idnat (idfun nat) = funExt nat (\(_ : nat) -> nat) idnat
   rem : (n : nat) -> Id nat (idnat n) n = split
     zero -> refl nat zero
     suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
+
+caseNat (A : U) (a0 aS : A) : nat -> A = split
+ zero -> a0
+ suc n -> aS
+
+caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n))
+            : (n:nat) -> P n = split
+ zero -> a0
+ suc n -> aS n
+
+znots (n : nat) : neg (Id nat zero (suc n)) =
+ \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero
+
+snotz (n : nat) : neg (Id nat (suc n) zero) =
+ \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h)
+
+natDec : (n m:nat) -> dec (Id nat n m) = split
+ zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m))
+ suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n))
+   (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))
+                 (sucInj n m) (natDec n m))
+
+natSet : set nat = hedberg nat natDec
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 23d17e2..c584fe6 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -1,5 +1,7 @@
 module prelude where
 
+-- Identity types
+
 Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
 
 refl (A : U) (a : A) : Id A a a = <i> a
@@ -18,6 +20,9 @@ subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
 substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
   Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e
 
+substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a =
+ subst A P b a (<i> p @ -i)
+
 singl (A : U) (a : A) : U = (x : A) * Id A a x
 
 contrSingl (A : U) (a b : A) (p : Id A a b) :
@@ -51,7 +56,11 @@ compDown (A : U) (a a' b b' : A)
          (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b =
  compUp A a' a b' b (inv A a a' p) (inv A b b' q)
 
-idfun (A : U) (a : A) : A = a
+lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =
+ <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]
+
+lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p)  (refl A b) =
+  <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]
 
 test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
 test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
@@ -113,7 +122,7 @@ setIsProp (A : U) (f g : set A) : Id (set A) f g =
  <i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
 
 propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
-       (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1 
+       (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1
   = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i
 
 IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
@@ -122,4 +131,28 @@ IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) :
 lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A)
          (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 =
   <i> (pP (p @ i) (transport (<j> P (p @ i /\ j)) b0)
-          (transport (<j> P (p @ i \/ -j)) b1)) @ i
\ No newline at end of file
+          (transport (<j> P (p @ i \/ -j)) b1)) @ i
+
+
+-- Basic data types
+
+data N0 =
+
+efq (A : U) : N0 -> A = split{}
+neg (A : U) : U = A -> N0
+
+data Unit = tt
+
+data or (A B : U) = inl (a : A)
+                  | inr (b : B)
+
+dec (A : U) : U = or A (neg A)
+
+discrete (A : U) : U = (a b : A) -> dec (Id A a b)
+
+injective (A B : U) (f : A -> B) : U =
+  (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1
+
+idfun (A : U) (a : A) : A = a
+
+and (A B : U) : U = (_ : A) * B
diff --git a/examples/susp.ctt b/examples/susp.ctt
index 161141d..c1212ce 100644
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -2,7 +2,9 @@ module susp where
 
 import circle
 
-data susp (A:U) = north | south | merid (a:A) @ north ~ south
+data susp (A : U) = north
+                  | south
+                  | merid (a:A) @ north ~ south
 
 -- n-spheres
 sphere : nat -> U = split
@@ -18,7 +20,7 @@ s1ToCircle : sone -> S1 = split
   south   -> base
   merid b @ i -> (path b) @ i
     where path : bool ->Id S1 base base = split
-            false -> loop'
+            false -> loop1
             true  -> refl S1 base
 
 m0 : Id sone north south = <i> (merid{sone} false) @ i
@@ -37,7 +39,7 @@ oc (x:S1) : S1 = s1ToCircle (circleToS1 x)
 
 ocid : (x : S1) -> Id S1 (oc x) x = split
     base -> refl S1 base
-    loop @ i -> <j> oc (loop' @ i)
+    loop @ i -> <j> oc (loop1 @ i)
 
 co (x: sone) : sone = circleToS1 (s1ToCircle x)
 
@@ -98,7 +100,7 @@ s1ToCId (p: Id sone north north) : Id S1 base base
 s1ToCIdInv (p : Id S1 base base) : Id sone north north
  = <i> (transport (<j> s1EqCircle @(-j)) (p @ i))
 
-loop1S :  Id sone north north = s1ToCIdInv loop'
+loop1S :  Id sone north north = s1ToCIdInv loop1
 
 loop2S : Id sone north north = compId sone north north north loop1S loop1S