clean mult

diff --git a/examples/mult.ctt b/examples/mult.ctt
index 4f3ccb982cbf3eb452a12874bdd0a42c32c8ac3f..d6f0f3744e767ec490ba9f62adc147762fde656c 100644 (file)
--- 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