auto gitdoc commit

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