From 2d2875e28d0116edcbd278576a6d152b18ba2319 Mon Sep 17 00:00:00 2001 From: coquand Date: Mon, 27 Apr 2015 21:44:41 +0200 Subject: [PATCH] clean mult --- examples/mult.ctt | 13 ------------- 1 file changed, 13 deletions(-) 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 (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 -- 2.34.1