ch 6

src/HottBook/Chapter2.lagda.md

@@ -181,7 +181,7 @@ record qinv {A B : Type} (f : A → B) : Type where
 ### Example 2.4.7
 
 ```
-id-qinv : qinv id
+id-qinv : {A : Type} → qinv {A} id
 id-qinv = record
   { g = id
   ; α = λ _ → refl

src/HottBook/Chapter6.lagda.md

@@ -0,0 +1,34 @@
+```
+module HottBook.Chapter6 where
+
+open import Relation.Binary.PropositionalEquality
+
+open import HottBook.Chapter2
+```
+
+### Definition 6.2.2 (Dependent paths)
+
+```
+dep-path : {A : Type} (P : A → Type) {x y : A} (p : x ≡ y)
+  → (u : P x) → (v : P y) → Type
+dep-path P p u v = transport P p u ≡ v
+```
+
+Circle definition
+
+```
+postulate
+  𝕊¹ : Type
+  base : 𝕊¹
+  loop : base ≡ base
+  𝕊¹-elim : (P : 𝕊¹ → Type) → (p-base : P base)
+    → (p-loop : dep-path P loop p-base p-base)
+    → (x : 𝕊¹) → P x
+```
+
+### Lemma 6.2.5
+
+```
+lemma625 : {A : Type} (a : A) → (p : a ≡ a) → 𝕊¹ → A
+lemma625 {A} a p circ = 𝕊¹-elim (λ _ → A) a ? circ
+```