From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 7 Jul 2016 11:47:31 +0000 (+0200)
Subject: merge mult and multS1
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=86ec6ce8016c9b9074dfa9defebf4ae8780e4003;p=cubicaltt.git

merge mult and multS1
---

diff --git a/examples/mult.ctt b/examples/mult.ctt
deleted file mode 100644
index 859805e..0000000
--- a/examples/mult.ctt
+++ /dev/null
@@ -1,46 +0,0 @@
-module mult where
-
-import circle
-
--- another inverse function
-
-invS : S1 -> S1 = split
- base -> base
- loop @ i -> loop1 @ -i
-
-test (x:S1) : S1 = mult x (invS x)
-testL : Id S1 base base = <i>test (loop{S1} @ i)
-test1 (x:S1) : S1 = mult (invS x) x
-
--- 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> base -- loop1 @ -i\/i\/j
-
-test2 : 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)
-test3 : loopS1 = <i> mult (loop1@i) (loop1@i)
--- 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)
-
--- corrInv (x y : S1) : Id S1 (mult x (mult (invS x) y)) y =
---  compId S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) y rem1 rem
---  where rem1 : Id S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) = multAssoc x (invS x) y
-
---        rem : Id S1 (mult (mult x (invS x)) y) y =
---         compId S1 (mult (mult x (invS x)) y) (mult base y) y  (<i>mult (lemInv x @i) y) (idL y)
-
--- corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
---  compId S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) y rem1 rem
---  where rem1 : Id S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) = multAssoc (invS x) x y
-
---        rem : Id S1 (mult (mult (invS x) x) y) y =
---         compId S1 (mult (mult (invS x) x) y) (mult base y) y (<i>mult (lemInv1 x@i) y) (idL y)
-
--- eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
-
diff --git a/examples/multS1.ctt b/examples/multS1.ctt
index b7e0cee..d7d3a3e 100644
--- a/examples/multS1.ctt
+++ b/examples/multS1.ctt
@@ -6,25 +6,6 @@ import circle
 
 -- the multiplication is invertible
 
-propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =
- <j>(p0 a1@j,
-     \ (x:A) -> 
-        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
-                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])
- where
-  a0 : A = z0.1
-  p0 : (x:A) -> Id A a0 x = z0.2
-  a1 : A = z1.1
-  p1 : (x:A) -> Id A a1 x = z1.2
-  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
- 
-propIsEquiv (A B : U) (f : A -> B)
-  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
-
-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) : IdP (<i>P (p@i)) b0 b1 =
- <i>pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (<j>P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i
-
 lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split
  base -> bP
  loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i
@@ -50,7 +31,7 @@ test1 : S1 = mapOnPath S1 S1 invS1 base base loop2@1
 
 test2 : Id S1 pt0 pt0 = mapOnPath S1 S1 invS1 base base loop2
 
-test2 : Id S1 pt0 pt0 = 
+ntest2 : Id S1 pt0 pt0 = 
   <i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 0) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ], (j = 1) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ]) []) [] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) base []) [ (j = 0) -> <k> comp (<_>S1) base [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (loop {S1} @ -j) []) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 0) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ], (j = 1) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [] ] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ]) []) [], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 1) -> <k> base ]) []) [], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 1) -> <k> base ]) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 0) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ], (k = 1) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 1) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 1) -> <l> base ]) []) [] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (loop {S1} @ -k) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 0) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ], (k = 1) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (k = 1) -> <l> comp (<_>S1) base [] ]) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ] ]
 
 -- invsone : sone -> sone  = subst U (\ (X:U) -> X -> X) <_>S1 sone (<i>s1EqCircle@-i) inv<_>S1
@@ -96,3 +77,50 @@ loopM2 : Id <_>S1 pt0 test1 = mapOnPath S1 S1 invS1 base base loop2
 loopM0 : Id S1 pt0 pt0 = <i>invMult (loop2@i) (loop2@i)
 -}
 
+
+-- mult:
+
+
+
+-- another inverse function
+
+invS : S1 -> S1 = split
+ base -> base
+ loop @ i -> loop1 @ -i
+
+test (x:S1) : S1 = mult x (invS x)
+testL : Id S1 base base = <i>test (loop{S1} @ i)
+test1 (x:S1) : S1 = mult (invS x) x
+
+-- 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> base -- loop1 @ -i\/i\/j
+
+test2 : 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)
+test3 : loopS1 = <i> mult (loop1@i) (loop1@i)
+-- 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)
+
+-- corrInv (x y : S1) : Id S1 (mult x (mult (invS x) y)) y =
+--  compId S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) y rem1 rem
+--  where rem1 : Id S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) = multAssoc x (invS x) y
+
+--        rem : Id S1 (mult (mult x (invS x)) y) y =
+--         compId S1 (mult (mult x (invS x)) y) (mult base y) y  (<i>mult (lemInv x @i) y) (idL y)
+
+-- corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
+--  compId S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) y rem1 rem
+--  where rem1 : Id S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) = multAssoc (invS x) x y
+
+--        rem : Id S1 (mult (mult (invS x) x) y) y =
+--         compId S1 (mult (mult (invS x) x) y) (mult base y) y (<i>mult (lemInv1 x@i) y) (idL y)
+
+-- eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
+