diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 3b6c1ca..b2da2fd 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -2,6 +2,14 @@
- [Front](./front.md)
+# HoTT Book
+
+- [Chapter 1](./generated/HottBook.Chapter1.md)
+- [Chapter 2](./generated/HottBook.Chapter2.md)
+- [Chapter 3](./generated/HottBook.Chapter3.md)
+- [Chapter 4](./generated/HottBook.Chapter4.md)
+- [Chapter 5](./generated/HottBook.Chapter5.md)
+
# HoTT Book (Cubical formulation)
- [Chapter 1](./generated/CubicalHott.Chapter1.md)
diff --git a/src/CEKCoinductive.agda b/src/CEKCoinductive.agda
new file mode 100644
index 0000000..42cf38f
--- /dev/null
+++ b/src/CEKCoinductive.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --guardedness #-}
+
+module CEKCoinductive where
+
+open import Agda.Primitive
+
+private
+ variable
+ l l1 l2 l3 : Level
+
+ E : Set → Set
+ R : Set
+
+data ITreeF (ITree : Set) : Set where
+ Ret : (r : R) → ITreeF ITree
+ Tau : (t : ITree) → ITreeF ITree
+ Vis : {A : Set l1} → (e : E A) → (k : A → ITreeF E R) → ITreeF E R
+
+record ITree : Set where
+ coinductive
+ field
+ _observe : ITreeF ITree
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md
index 09959ff..7903742 100644
--- a/src/CubicalHott/Chapter6.lagda.md
+++ b/src/CubicalHott/Chapter6.lagda.md
@@ -6,6 +6,21 @@ open import CubicalHott.Chapter1
open import CubicalHott.Chapter2
```
+## 6.3 The interval
+
+```
+data Iv : Type where
+ 0I : Iv
+ 1I : Iv
+ seg : 0I ≡ 1I
+```
+
+### Lemma 6.3.1
+
+```
+lemma6∙3∙1 : isContr Iv
+```
+
## 6.4 Circles and spheres
```
@@ -18,36 +33,36 @@ data S¹ : Type where
```
lemma6∙4∙1 : loop ≢ refl
-lemma6∙4∙1 p =
- {! !}
- where
- open ≡-Reasoning
+-- lemma6∙4∙1 p =
+-- {! !}
+-- where
+-- open ≡-Reasoning
- f : {A : Type} (x : A) → (p : x ≡ x) → S¹ → A
- f x p base = x
- f x p (loop i) = p i
+-- f : {A : Type} (x : A) → (p : x ≡ x) → S¹ → A
+-- f x p base = x
+-- f x p (loop i) = p i
- bad : {A : Type} (x : A) → (p : x ≡ x) → p ≡ refl
- bad x p = begin
- p ≡⟨ {! !} ⟩
- p ≡⟨ {! !} ⟩
- refl ∎
+-- bad : {A : Type} (x : A) → (p : x ≡ x) → p ≡ refl
+-- bad x p = begin
+-- p ≡⟨ {! !} ⟩
+-- p ≡⟨ {! !} ⟩
+-- refl ∎
```
### Lemma 6.4.2
```
lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl))
-lemma6∙4∙2 = f , g
- where
- f : (x : S¹) → x ≡ x
- f base = loop
- f (loop i) i₁ = loop {! !}
+-- lemma6∙4∙2 = f , g
+-- where
+-- f : (x : S¹) → x ≡ x
+-- f base = loop
+-- f (loop i) i₁ = loop {! !}
- g : f ≢ (λ x → refl)
- g p = let
- z = happlyd p
- z2 = z base
- z3 = lemma6∙4∙1 z2
- in z3
+-- g : f ≢ (λ x → refl)
+-- g p = let
+-- z = happlyd p
+-- z2 = z base
+-- z3 = lemma6∙4∙1 z2
+-- in z3
```
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 84c351f..d557ff4 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -724,11 +724,8 @@ module axiom2∙10∙3 where
postulate
ua : {l : Level} {A B : Set l} → (A ≃ B) → (A ≡ B)
- forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
- -- forward eqv = {! !}
-
backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
- -- backward p = {! !}
+ forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 159f91a..9463dec 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -184,18 +184,8 @@ theorem3∙2∙2 double-neg = conclusion
let y = what ∙ x in
sym y ∙ foranyu
- -- postulate
- huhh : (Σ.fst e) (fbool u) ≡ fbool u
- huhh =
- let
- equiv1 = ap ua (axiom2∙10∙3.forward e)
-
- x : {A B : Set l} → (e : A ≃ B) → (a : A) → transport id (ua e) a ≡ Σ.fst e a
- x e a =
- {! axiom2∙10∙3.forward ? !}
- in
- {! !}
- -- sym (x e (fbool u)) ∙ nextStep
+ postulate
+ huhh : (Σ.fst e) (fbool u) ≡ fbool u
finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
finalStep (lift true) p =
@@ -310,5 +300,9 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
concat : g (∣ g x ∣) ≡ g (∣ g y ∣)
concat = a ∙ eqProp ∙ (sym b)
in
- {! prop ? !}
+ admit
+ where
+ postulate
+ -- TODO: Finish this
+ admit : x ≡ y
```
\ No newline at end of file
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
new file mode 100644
index 0000000..a1d501b
--- /dev/null
+++ b/src/HottBook/Chapter6.lagda.md
@@ -0,0 +1,53 @@
+```
+module HottBook.Chapter6 where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3
+
+private
+ variable
+ l : Level
+```
+
+# Chapter 6 Higher Inductive Types
+
+```
+postulate
+ S¹ : Set
+ base : S¹
+ loop : base ≡ base
+```
+
+## 6.2 Induction principles and dependent paths
+
+```
+dep-path : {A : Set} {x y : A} → (P : A → Set) → (p : x ≡ y) → (u : P x) → (v : P y) → Set
+dep-path P p u v = transport P p u ≡ v
+
+syntax dep-path P p u v = u ≡[ P , p ] v
+```
+
+## 6.3 The interval
+
+```
+postulate
+ I : Set
+ 0I : I
+ 1I : I
+ seg : 0I ≡ 1I
+
+record I-rec (B : Set) (b0 b1 : B) (s : b0 ≡ b1) : Set where
+ field
+ f : I → B
+ prop1 : f 0I ≡ b0
+ prop2 : f 1I ≡ b1
+ prop3 : apd f seg ≡ {! s !}
+
+record I-ind (P : I → Set) (b0 : P 0I) (b1 : P 1I) (s : b0 ≡[ P , seg ] b1) : Set where
+ field
+ f : (x : I) → P x
+ prop1 : f 0I ≡ b0
+ prop2 : f 1I ≡ b1
+ prop3 : apd f seg ≡ {! s !}
+```
\ No newline at end of file
diff --git a/src/Hurewicz.agda b/src/Hurewicz.agda
new file mode 100644
index 0000000..06773e1
--- /dev/null
+++ b/src/Hurewicz.agda
@@ -0,0 +1,2 @@
+module Hurewicz where
+