From 1368b9e2c935b3e61a80db72fe2c04266eb5a84e Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 17 May 2023 03:02:38 -0500
Subject: [PATCH] ch 6

---
 src/HottBook/Chapter2.lagda.md |  2 +-
 src/HottBook/Chapter6.lagda.md | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 src/HottBook/Chapter6.lagda.md

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 6fc41c4..68256ee 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/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
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
new file mode 100644
index 0000000..09a505f
--- /dev/null
+++ b/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
+```