Tweak s3-join-s3. (#298)

* Follow the Geometry. * Algebraic simplification.
RedPRL · Sep 7, 2018 · 6cf9d6a · 6cf9d6a
1 parent 97fa960
commit 6cf9d6a
Showing 1 changed file with 0 additions and 14 deletions.
diff --git a/example/s3-to-join.red b/example/s3-to-join.red
@@ -133,35 +133,21 @@ let s3-join-s3 (d : s3) : Path s3 (join-to-s3 (s3-to-join d)) d =
   elim d [
   | base → refl
   | cube i j k → λ x →
-    let cnx/image : (i m : dim) → s3 =
-      λ i m → comp 0 i base [ m=0 → refl | m=1 → refl ]
-    in
     let cnx/filler : (i m x : dim) → s3 =
       λ i m x →
         comp 0 i base
         [ m=0 → refl
         | m=1 → refl
-        | x=0 i → cnx/image i m
         | x=1 → refl
         ]
     in
-    let k01/image : (i m : dim) → s3 =
-      λ i m →
-        comp 1 i (cnx/image 1 m) [
-        | j=0 i → cnx/image i m
-        | j=1 i → cnx/image i m
-        | m=0 → refl
-        | m=1 → refl
-        ]
-    in
     let k01/filler : (i m x : dim) → s3 =
       λ i m x →
        comp 1 i (cnx/filler 1 m x) [
        | j=0 i → cnx/filler i m x
        | j=1 i → cnx/filler i m x
        | m=0 → refl
        | m=1 → refl
-       | x=0 i → k01/image i m
        | x=1 → refl
        ]
     in