From 2d8f88d69ae6228ab457cf3218a2148b528d7e33 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 02:47:47 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 7294291..5dbe4b4 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -234,6 +234,19 @@ record isequiv {A B : Set} (f : A → B) : Set where
     h-id : h ∘ f ∼ id
 ```
 
+```
+qinv-to-isequiv : {A B : Set}
+  → {f : A → B}
+  → qinv f
+  → isequiv f
+qinv-to-isequiv q = record
+  { g = qinv.g q
+  ; g-id = qinv.α q
+  ; h = qinv.g q
+  ; h-id = {! qinv.β q  !}
+  }
+```
+
 ### Definition 2.4.11
 
 ```
@@ -317,7 +330,16 @@ idToEquiv {A} {B} p = func , equiv
         wtf2 : (func ∘ func-inv) ≡ wtf
         wtf2 = refl
 
+        wtf3 : A → A
         wtf3 = J (λ A' B' p' → A' → A') (λ A' → id) A B p
+
+        wtf3-qinv : qinv wtf3
+        wtf3-qinv = record
+          { g = wtf3
+          ; α = λ _ → refl
+          ; β = λ _ → refl
+          }
+
       in {!    !}
 
     equiv = record