auto gitdoc commit

src/HottBook/Chapter2.lagda.md

@@ -406,13 +406,14 @@ theorem2∙13∙1 m n = encode m n , equiv
     backward (suc m) (suc n) c =
       let
         IH = backward m n c
-        what : code m n
+
+        -- what : code m n
         -- what = encode (suc m) (suc n) (ap suc (decode m n c))
         -- what = transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m))
         -- what = transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m))
         -- what = transport (λ n → code m n) (decode m n c) (r m)
         -- what = transport (λ n → code m n) (decode m n c) (r m)
-        what = transport (λ n → code m n) (decode m n c) (r m)
+        -- what = transport (λ n → code m n) (decode m n c) (r m)
 
         res2 : transport (λ x → code (suc m) (suc x)) (decode m n c) (r (suc m)) ≡ c
         res2 = IH