From eb53383a785a41e3b8e2134080e6e3fbcb10a77c Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 04:29:53 +0000
Subject: [PATCH] auto gitdoc commit
---
src/HottBook/Chapter2.lagda.md | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 08607df..00c8dec 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/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