Update 06-contractible.rzk.md

rzk-lang · Jun 17, 2024 · 7e5805b · 7e5805b
1 parent 5ced160
commit 7e5805b
Showing 1 changed file with 0 additions and 8 deletions.
diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
@@ -568,9 +568,7 @@ type evaluated at the point of contraction.
   → ( Σ ( x : A) , C x)
   :=
     \ v → ((center-contraction A is-contr-A) , v)
-```
 
-```rzk
 #def total-type-to-second-center-is-contr-base
   ( A : U)
   ( is-contr-A : is-contr A)
@@ -590,9 +588,7 @@ type evaluated at the point of contraction.
           ( x)
           ( homotopy-contraction A is-contr-A x))
         ( u)
-```
 
-```rzk
 #def has-retraction-total-type-to-second-center-is-contr-base
   ( A : U)
   ( is-contr-A : is-contr A)
@@ -617,9 +613,7 @@ type evaluated at the point of contraction.
               ( x)
               ( homotopy-contraction A is-contr-A x))
             ( u))))
-```
 
-```rzk
 #def has-section-total-type-to-second-center-is-contr-base
   ( A : U)
   ( is-contr-A : is-contr A)
@@ -672,9 +666,7 @@ type evaluated at the point of contraction.
           ( ( center-contraction A is-contr-A) , u)
           ( ( center-contraction A is-contr-A) , u)
           ( refl))))
-```
 
-```rzk
 #def equiv-total-type-second-center-is-contr-base
   ( A : U)
   ( is-contr-A : is-contr A)