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

---
 src/HottBook/Chapter2.lagda.md | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index c1ad14a..50ce83f 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -149,12 +149,12 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
 ### Lemma 2.3.11
 
 ```
-lemma2∙3∙11 : {A : Set} {P Q : A → Set}
-  → (f : (x : A) → P x → Q x)
-  → {x y : A} (p : x ≡ y) → (u : P x)
-  → transport Q p (f x u) ≡ f y (transport P p u)
-lemma2∙3∙11 {A} {P} {Q} f {x} {y} p u =
-  J (λ a b p → transport Q p (f a {!   !}) ≡ f b (transport P p {!   !})) (λ a → {!   !}) x y p
+-- lemma2∙3∙11 : {A : Set} {P Q : A → Set}
+--   → (f : (x : A) → P x → Q x)
+--   → {x y : A} (p : x ≡ y) → (u : P x)
+--   → transport Q p (f x u) ≡ f y (transport P p u)
+-- lemma2∙3∙11 {A} {P} {Q} f {x} {y} p u =
+--   J (λ a b p → transport Q p (f a {!   !}) ≡ f b (transport P p {!   !})) (λ a → {!   !}) x y p
   -- J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
 ```
 
@@ -295,8 +295,17 @@ postulate
 ### Lemma 2.10.1
 
 ```
--- idToEquiv : {A B : Set} → (A ≡ B) → A ≃ B
--- idToEquiv p = ? , ?
+idToEquiv : {A B : Set}
+  → (A ≡ B)
+  → A ≃ B
+idToEquiv {A} {B} p = {!   !} , equiv
+  where
+    equiv = record
+      { g = {!   !}
+      ; g-id = {!   !}
+      ; h = {!   !}
+      ; h-id = {!   !}
+      }
 ```
 
 ### Axiom 2.10.3 (Univalence)