From 4ecd3f7c9375f599ef25fc817b4c71b3baa057cc Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 22 Apr 2024 03:24:01 +0000 Subject: [PATCH] auto gitdoc commit --- src/HottBook/Chapter2.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 0c43b58..8b8e3fd 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -390,7 +390,9 @@ theorem2∙13∙1 m n = encode m n , equiv c : (x : ℕ) → decode x x (r x) ≡ refl c zero = refl - c (suc x) = {! !} + c (suc x) = + let wtf = c x in + {! !} equiv = record { g = decode m n