auto gitdoc commit

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)