diff --git a/html/Agda.css b/html/Agda.css
new file mode 100644
index 0000000..656783c
--- /dev/null
+++ b/html/Agda.css
@@ -0,0 +1,41 @@
+/* Aspects. */
+.content .Agda .Comment { color: #B22222 }
+.content .Agda .Background {}
+.content .Agda .Markup { color: #000000 }
+.content .Agda .Keyword { color: #CD6600 }
+.content .Agda .String { color: #B22222 }
+.content .Agda .Number { color: #A020F0 }
+.content .Agda .Symbol { color: #404040 }
+.content .Agda .PrimitiveType { color: #0000CD }
+.content .Agda .Pragma { color: black }
+.content .Agda .Operator {}
+.content .Agda .Hole { background: #B4EEB4 }
+
+/* NameKinds. */
+.content .Agda .Bound { color: black }
+.content .Agda .Generalizable { color: black }
+.content .Agda .InductiveConstructor { color: #008B00 }
+.content .Agda .CoinductiveConstructor { color: #8B7500 }
+.content .Agda .Datatype { color: #0000CD }
+.content .Agda .Field { color: #EE1289 }
+.content .Agda .Function { color: #0000CD }
+.content .Agda .Module { color: #A020F0 }
+.content .Agda .Postulate { color: #0000CD }
+.content .Agda .Primitive { color: #0000CD }
+.content .Agda .Record { color: #0000CD }
+
+/* OtherAspects. */
+.content .Agda .DottedPattern {}
+.content .Agda .UnsolvedMeta { color: black; background: yellow }
+.content .Agda .UnsolvedConstraint { color: black; background: yellow }
+.content .Agda .TerminationProblem { color: black; background: #FFA07A }
+.content .Agda .IncompletePattern { color: black; background: #F5DEB3 }
+.content .Agda .Error { color: red; text-decoration: underline }
+.content .Agda .TypeChecks { color: black; background: #ADD8E6 }
+.content .Agda .Deadcode { color: black; background: #808080 }
+.content .Agda .ShadowingInTelescope { color: black; background: #808080 }
+
+/* Standard attributes. */
+.Agda a { text-decoration: none }
+.Agda a[href]:hover { background-color: #B4EEB4 }
+.Agda [href].hover-highlight { background-color: #B4EEB4; }
diff --git a/html/book.toml b/html/book.toml
index a46ad34..69bb4db 100644
--- a/html/book.toml
+++ b/html/book.toml
@@ -5,8 +5,17 @@ multilingual = false
src = "src"
title = "HoTT Book"
-[preprocessor.pagetoc]
+[preprocessor.katex]
+command = "mdbook-katex"
+
+# [preprocessor.pagetoc]
[output.html]
-additional-js = ["theme/pagetoc.js"]
-additional-css = ["src/generated/Agda.css", "style.css", "theme/pagetoc.css"]
+additional-js = [
+ # "theme/pagetoc.js"
+]
+additional-css = [
+ "Agda.css",
+ "style.css",
+ # "theme/pagetoc.css"
+]
diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 22b9b34..fd3133a 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -1,7 +1,10 @@
# Summary
- [Chapter 1](./generated/HottBook.Chapter1.md)
+ - [Exercises](./generated/HottBook.Chapter1Exercises.md)
- [Chapter 2](./generated/HottBook.Chapter2.md)
+ - [Exercises](./generated/HottBook.Chapter2Exercises.md)
- [Chapter 3](./generated/HottBook.Chapter3.md)
- [Chapter 4](./generated/HottBook.Chapter4.md)
-- [Chapter 5](./generated/HottBook.Chapter5.md)
\ No newline at end of file
+- [Chapter 5](./generated/HottBook.Chapter5.md)
+- [Chapter 6](./generated/HottBook.Chapter6.md)
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 05782c4..170f05b 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -6,11 +6,14 @@ module HottBook.Chapter2 where
open import Agda.Primitive
open import HottBook.Chapter1
+open import HottBook.Chapter2Lemma221
open import HottBook.Util
```
+# 2 Homotopy type theory
+
## 2.1 Types are higher groupoids
### Lemma 2.1.1
@@ -33,6 +36,8 @@ trans {l} {A} {x} {y} {z} p q =
func1 x y p = J (λ a b p → a ≡ b) (λ x → refl) x y p
func2 = J (λ a b p → (z : A) → (q : b ≡ z) → a ≡ z) func1 x y p
in func2 z q
+
+infixr 30 _∙_
_∙_ = trans
```
@@ -60,25 +65,37 @@ module ≡-Reasoning where
### Lemma 2.1.4
```
-record lemma2∙1∙4-statement {A : Set} {x y z w : A}
- (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) : Set where
- field
- i1 : p ≡ p ∙ refl
- i2 : p ≡ refl ∙ p
- ii1 : (sym p) ∙ p ≡ refl
- ii2 : p ∙ (sym p) ≡ refl
- iii : sym (sym p) ≡ p
- iv : p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+module lemma2∙1∙4 {A : Set} where
+ i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
+ i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
-lemma2∙1∙4 : {A : Set} {x y z w : A}
- → (p : x ≡ y)
- → (q : y ≡ z)
- → (r : z ≡ w)
- → lemma2∙1∙4-statement p q r
+ i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
+ i2 {x} {y} p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
+
+ ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
+ ii1 {x} {y} p = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
+
+ ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl
+ ii2 {x} {y} p = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
+
+ iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
+ iii {x} {y} p = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
+
+ iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+ iv {x} {y} {z} {w} p q r = let
+ open ≡-Reasoning
+
+ C : (x y : A) → (p : x ≡ y) → Set
+ C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+
+ c : (x : A) → C x x refl
+ c x q1 = begin
+ refl ∙ (q1 ∙ r) ≡⟨ sym (i2 (q1 ∙ r)) ⟩
+ (q1 ∙ r) ≡⟨ ap (λ p → p ∙ r) (i2 q1) ⟩
+ (refl ∙ q1) ∙ r ∎
+ in J C c x y p q
```
-(Proof appears below ap)
-
### Definition 2.1.7 (pointed type)
This comes first, since it is needed to define Theorem 2.1.6.
@@ -112,51 +129,18 @@ TODO
### Lemma 2.2.1
-```
-ap : {l : Level} {A B : Set l} {x y : A}
- → (f : A → B)
- → (p : x ≡ y)
- → f x ≡ f y
-ap {l} {A} {B} {x} {y} f p = J (λ x y p → f x ≡ f y) (λ x → refl) x y p
-```
+{{#include HottBook.Chapter2Lemma221.md:ap}}
-
- Proof of Lemma 2.1.4
+### Lemma 2.2.2
+
+Ap rules
```
-
-lemma2∙1∙4 {A} {x} {y} {z} {w} p q r =
- let
- i2 : (x y : A) (p : x ≡ y) → p ≡ refl ∙ p
- i2 x y p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
- in record
- { i1 = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
- ; i2 = i2 x y p
- ; ii1 = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
- ; ii2 = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
- ; iii = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
- ; iv =
- let
- C : (x y : A) → (p : x ≡ y) → Set
- C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
-
- wtf : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ (refl ∙ (q1 ∙ r))
- wtf x q1 = i2 x w (q1 ∙ r)
-
- wtf2 : (x : A) (q1 : x ≡ z) → q1 ≡ (refl ∙ q1)
- wtf2 x q1 = i2 x z q1
-
- wtf3 : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ ((refl ∙ q1) ∙ r)
- wtf3 x q1 = ap (λ x → x ∙ r) (wtf2 x q1)
-
- c : (x : A) → C x x refl
- c x q1 = trans (sym (wtf x q1)) (wtf3 x q1)
- in J C c x y p q
- }
+-- module lemma2∙2∙2 {A B : Set} {f : A → B} {x y z : A} {p : x ≡ y} {q : y ≡ z} where
+-- i : ap f (p ∙ q) ≡ ap f p ∙ ap f q
+-- i = J ((λ x1 y1 p1 → (q1 : y1 ≡ z) → ap f (p1 ∙ q1) ≡ ap f p1 ∙ ap f q1)) (λ x1 q1 → {! !}) x y p q
```
-
-
## 2.3 Type families are fibrations
### Lemma 2.3.1 (Transport)
@@ -240,11 +224,7 @@ lemma2∙3∙9 {A} {x} {y} {z} P p q u =
let
f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1
f2 x1 q1 u1 =
- let
- properties = lemma2∙1∙4 q1 refl refl
- property = lemma2∙1∙4-statement.i2 properties
- in
- ap (λ x → transport P x u1) property
+ ap (λ x → transport P x u1) (lemma2∙1∙4.i2 q1)
f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p
in f1 q u
```
@@ -354,14 +334,10 @@ transport-qinv : {A : Set}
transport-qinv P p = mkQinv (transport P (sym p))
(λ py →
let wtf = lemma2∙3∙9 P (sym p) p py in
- let properties = lemma2∙1∙4 p refl refl in
- let property = lemma2∙1∙4-statement.ii1 properties in
- trans wtf (ap (λ x → transport P x py) property))
+ trans wtf (ap (λ x → transport P x py) (lemma2∙1∙4.ii1 p)))
(λ px →
let wtf = lemma2∙3∙9 P p (sym p) px in
- let properties = lemma2∙1∙4 p refl refl in
- let property = lemma2∙1∙4-statement.ii2 properties in
- trans wtf (ap (λ x → transport P x px) property))
+ trans wtf (ap (λ x → transport P x px) (lemma2∙1∙4.ii2 p)))
```
### Definition 2.4.10
@@ -413,44 +389,45 @@ A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
### Lemma 2.4.12
```
-id-equiv : (A : Set) → A ≃ A
-id-equiv A = id , e
- where
- e : isequiv id
- e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
+module lemma2∙4∙12 where
+ id-equiv : (A : Set) → A ≃ A
+ id-equiv A = id , e
+ where
+ e : isequiv id
+ e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
-sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
-sym-equiv {A} {B} (f , eqv) =
- let (mkQinv g α β) = isequiv-to-qinv eqv
- in g , qinv-to-isequiv (mkQinv f β α)
+ sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
+ sym-equiv {A} {B} (f , eqv) =
+ let (mkQinv g α β) = isequiv-to-qinv eqv
+ in g , qinv-to-isequiv (mkQinv f β α)
-trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
-trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
- let
- (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
- (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
+ trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
+ trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
+ let
+ (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
+ (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
- open ≡-Reasoning
+ open ≡-Reasoning
- forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
- forward c =
- begin
- ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
- (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
- (g ∘ id ∘ g-inv) c ≡⟨⟩
- (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
- id c ∎
+ forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
+ forward c =
+ begin
+ ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
+ (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
+ (g ∘ id ∘ g-inv) c ≡⟨⟩
+ (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
+ id c ∎
- backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
- backward a =
- begin
- ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
- (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
- (f-inv ∘ (id ∘ f)) a ≡⟨⟩
- (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
- id a ∎
-
- in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
+ backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
+ backward a =
+ begin
+ ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
+ (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
+ (f-inv ∘ (id ∘ f)) a ≡⟨⟩
+ (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
+ id a ∎
+
+ in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
```
## 2.7 Σ-types
@@ -578,15 +555,25 @@ postulate
### Theorem 2.11.1
```
-theorem2∙11∙1 : {A B : Set}
- → (eqv @ (f , f-eqv) : A ≃ B)
- → (a a' : A)
- → (a ≡ a') ≃ (f a ≡ f a')
-theorem2∙11∙1 (f , mkIsEquiv g g-id h h-id) a a' = ap f , qinv-to-isequiv eqv
- where
- inv : f a ≡ f a' → a ≡ a'
- inv p = trans {! !} (trans (ap g p) {! !})
- eqv = mkQinv {! !} {! !} {! !}
+-- theorem2∙11∙1 : {A B : Set}
+-- → (eqv @ (f , f-eqv) : A ≃ B)
+-- → (a a' : A)
+-- → (a ≡ a') ≃ (f a ≡ f a')
+-- theorem2∙11∙1 (f , f-eqv) a a' =
+-- let
+-- open ≡-Reasoning
+-- mkQinv f⁻¹ α β = isequiv-to-qinv f-eqv
+-- inv : (f a ≡ f a') → a ≡ a'
+-- inv p = (sym (β a)) ∙ (ap f⁻¹ p) ∙ (β a')
+-- backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
+-- backward q = begin
+-- ap f ((sym (β a)) ∙ (ap f⁻¹ q) ∙ (β a')) ≡⟨ {! !} ⟩
+-- id q ∎
+-- forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
+-- forward p = {! !}
+-- eqv = mkQinv inv backward forward
+-- in
+-- ap f , qinv-to-isequiv eqv
```
## 2.13 Natural numbers
@@ -686,4 +673,4 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
where
g : (X → A) × (X → B) → (X → A × B)
g (f1 , f2) = λ x → (f1 x , f2 x)
-```
\ No newline at end of file
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index c8ee1c0..f3eb6da 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -27,7 +27,7 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
[2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6
[2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7
-### Exercise 2.13
+## Exercise 2.13
_Show that $(2 \simeq 2) \simeq 2$._
@@ -81,11 +81,11 @@ exercise2∙13 = f , equiv
g true = id , id-equiv
g false = neg , neg-equiv
- f∘g∼id : f ∘ g ∼ id
+ f∘g∼id : (f ∘ g) ∼ id
f∘g∼id true = refl
f∘g∼id false = refl
- g∘f∼id : g ∘ f ∼ id
+ g∘f∼id : (g ∘ f) ∼ id
g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = attempt
where
Bmap : 𝟚 → Set
diff --git a/src/HottBook/Chapter2Lemma221.lagda.md b/src/HottBook/Chapter2Lemma221.lagda.md
new file mode 100644
index 0000000..cb9d840
--- /dev/null
+++ b/src/HottBook/Chapter2Lemma221.lagda.md
@@ -0,0 +1,19 @@
+```
+module HottBook.Chapter2Lemma221 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+```
+
+[]: ANCHOR: ap
+
+```
+ap : {l : Level} {A B : Set l} {x y : A}
+ → (f : A → B)
+ → (p : x ≡ y)
+ → f x ≡ f y
+ap {l} {A} {B} {x} {y} f p =
+ J (λ x y p → f x ≡ f y) (λ x → refl) x y p
+```
+
+[]: ANCHOR_END: ap
\ No newline at end of file
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 0620f14..8211f3f 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -5,6 +5,8 @@ open import HottBook.Chapter1
open import HottBook.Chapter2
```
+# 6 Higher inductive types
+
### Definition 6.2.2 (Dependent paths)
```
@@ -31,7 +33,7 @@ postulate
### Lemma 6.2.5
-```text
+```
lemma6∙2∙5 : {A : Set}
→ (a : A)
→ (p : a ≡ a)
@@ -45,7 +47,7 @@ lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ
p-loop : transport P loop a ≡ a
p-loop =
- let wtf = {! lemma2∙3∙8 !} in
+ let wtf = lemma2∙3∙8 loop in
{! !}
```
@@ -62,8 +64,8 @@ postulate
## 6.10 Quotients
```
-module Quotient (A : Set) (R : A × A → Prop) where
- postulate
- _/_ : Set → Set → Set
- q : (A : Set) → A / A
+-- module Quotient (A : Set) (R : A × A → Prop) where
+-- postulate
+-- _/_ : Set → Set → Set
+-- q : (A : Set) → A / A
```
\ No newline at end of file
diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index 31534f2..b951e37 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -16,6 +16,6 @@ data ℤ : Set where
```
```
-code : {l : Level} → S¹ → Set (lsuc l)
-code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
+-- code : {l : Level} → S¹ → Set (lsuc l)
+-- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
```
\ No newline at end of file