From: coquand <coquand@chalmers.se>
Date: Mon, 27 Apr 2015 19:44:41 +0000 (+0200)
Subject: clean mult
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=2d2875e28d0116edcbd278576a6d152b18ba2319;p=cubicaltt.git

clean mult
---

diff --git a/examples/mult.ctt b/examples/mult.ctt
index 4f3ccb9..d6f0f37 100644
--- a/examples/mult.ctt
+++ b/examples/mult.ctt
@@ -28,14 +28,6 @@ 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 (y:S1) : (x : S1) -> Id S1 (mult x (mult (invS x) y)) y = split
- base -> lemBase y
- loop @ i -> rem
-   where rem : Id S1 (mult (loop {S1} @ i) (mult (loop {S1} @ -i) y)) y =
-           transport (<j>Id S1 (mult (loop {S1} @ i/\j) (mult (loop {S1} @ -(i/\j)) y)) y) (lemBase 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
@@ -52,8 +44,3 @@ corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
 
 eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
 
--- we deduce the following fibration
-
-fibS1 (x:S1) : S1 -> U = split
- base -> S1
- loop @ i -> (eqS1 x) @ i