removed comments

jonalfcam · Sep 22, 2023 · 7af1390 · 7af1390
1 parent d1a17b7
commit 7af1390
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
@@ -512,16 +512,15 @@ to the point of contraction for weak extension extensionality.
       ((t : ψ ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
   := 
     first 
-    ( axiom-choice --- apply the forward equivalence of AoC
+    ( axiom-choice 
       ( I )
       ( ψ ) 
       ( ϕ ) 
       ( A ) 
       ( \ t y → y = b t)
       ( a ) 
       ( e ))  
-    ( first --- to the center of a contractible extension type
-             --- obtained from weak-ext-ext
+    ( first 
       ( weak-ext-ext 
         ( I )
         ( ψ )