diff --git a/html/style.css b/html/style.css
index 2a60e08..922465e 100644
--- a/html/style.css
+++ b/html/style.css
@@ -6,6 +6,6 @@
format("woff2");
}
-pre.Agda {
+pre.Agda, pre code {
font-family: "PragmataPro Mono Liga", monospace;
}
\ No newline at end of file
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index 2969f37..16b7864 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -100,6 +100,12 @@ data ๐ : Set where
false : ๐
```
+```
+neg : ๐ โ ๐
+neg true = false
+neg false = true
+```
+
## 1.9 The natural numbers
```
@@ -116,6 +122,7 @@ rec-โ C z s (suc n) = s n (rec-โ C z s n)
## 1.11 Propositions as types
```
+infix 3 ยฌ_
ยฌ_ : {l : Level} (A : Set l) โ Set l
ยฌ A = A โ โฅ
```
@@ -161,7 +168,7 @@ composite f g x = g (f x)
-- https://agda.github.io/agda-stdlib/master/Function.Base.html
infixr 9 _โ_
-_โ_ : {l : Level} {A B C : Set l}
+_โ_ : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3}
โ (g : B โ C)
โ (f : A โ B)
โ A โ C
diff --git a/src/HottBook/Chapter1Util.agda b/src/HottBook/Chapter1Util.agda
index 9c9dfc0..d6dbb9c 100644
--- a/src/HottBook/Chapter1Util.agda
+++ b/src/HottBook/Chapter1Util.agda
@@ -10,3 +10,10 @@ open import HottBook.Util
โ ฮฃ (aโ โก aโ) (ฮป p โ transport B p bโ โก bโ)
โ pโ โก pโ
ฮฃ-โก {lโ} {lโ} {A} {B} {pโ @ (aโ , bโ)} {pโ @ (aโ , bโ)} (refl , refl) = refl
+
+neg-homotopy : (neg โ neg) โผ id
+neg-homotopy true = refl
+neg-homotopy false = refl
+
+neg-equiv : ๐ โ ๐
+neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index edd8c0c..359dd72 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -385,7 +385,7 @@ transport-qinv P p = mkQinv (transport P (sym p))
### Definition 2.4.10
```
-record isequiv {l : Level} {A B : Set l} (f : A โ B) : Set l where
+record isequiv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A โ B) : Set (l1 โ l2) where
eta-equality
constructor mkIsEquiv
field
@@ -424,7 +424,7 @@ isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) =
### Definition 2.4.11
```
-_โ_ : {l : Level} โ (A B : Set l) โ Set l
+_โ_ : {l1 l2 : Level} โ (A : Set l1) (B : Set l2) โ Set (l1 โ l2)
A โ B = ฮฃ[ f โ (A โ B) ] (isequiv f)
```
@@ -637,11 +637,11 @@ postulate
```
happly : {A B : Set}
- โ (f g : A โ B)
- โ {x : A}
+ โ {f g : A โ B}
โ (p : f โก g)
+ โ (x : A)
โ f x โก g x
-happly {A} {B} f g {x} p = ap (ฮป h โ h x) p
+happly {A} {B} {f} {g} p x = ap (ฮป h โ h x) p
```
### Axiom 2.9.3 (Function extensionality)
@@ -654,6 +654,19 @@ postulate
โ f โก g
```
+### Equation 2.9.4
+
+```
+equation2โ9โ4 : {l1 l2 : Level} {X : Set l1} {x1 x2 : X}
+ โ {A B : X โ Set l2}
+ โ (f : A x1 โ B x1)
+ โ (p : x1 โก x2)
+ โ transport (ฮป x โ A x โ B x) p f โก ฮป x โ transport B p (f (transport A (sym p) x))
+equation2โ9โ4 {l1} {l2} {X} {x1} {x2} {A} {B} f p =
+ J (ฮป x3 y3 p1 โ (f1 : A x3 โ B x3) โ (transport (ฮป x โ A x โ B x) p1 f1 โก ฮป x โ transport B p1 (f1 (transport A (sym p1) x))))
+ (ฮป x3 f1 โ refl) x1 x2 p f
+```
+
### Lemma 2.9.6
```
@@ -697,7 +710,7 @@ idtoeqv {l} {A} {B} p = J C c A B p
```
module axiom2โ10โ3 where
postulate
- -- ua-eqv : {l : Level} {A B : Set l} โ (A โ B) โ (A โก B)
+ -- ua-eqv : {l1 l2 : Level} {A : Set l1} {B : Set l2} โ (A โ B) โ (A โก B)
ua : {l : Level} {A B : Set l} โ (A โ B) โ (A โก B)
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 8979f1d..7292f4b 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -46,25 +46,14 @@ isSet A = (x y : A) โ (p q : x โก y) โ p โก q
```
example3โ1โ9 : ยฌ (isSet Set)
-example3โ1โ9 p = {! !}
+example3โ1โ9 p = remark2โ12โ6 lol
where
open axiom2โ10โ3
- f : ๐ โ ๐
- f true = false
- f false = true
-
- f-homotopy : (f โ f) โผ id
- f-homotopy true = refl
- f-homotopy false = refl
-
- f-equiv : ๐ โ ๐
- f-equiv = f , qinv-to-isequiv (mkQinv f f-homotopy f-homotopy)
-
f-path : ๐ โก ๐
- f-path = ua f-equiv
+ f-path = ua neg-equiv
- bogus : f โก id
+ bogus : id โก neg
bogus =
let
helper : f-path โก refl
@@ -75,15 +64,67 @@ example3โ1โ9 p = {! !}
wtf : idtoeqv f-path โก idtoeqv refl
wtf = ap idtoeqv helper
in {! !}
+
+ lol : true โก false
+ lol = ap (ฮป f โ f true) bogus
```
## 3.2 Propositions as types?
### Theorem 3.2.2
+TODO: Study this more
+
```
-theorem3โ2โ2 : ((A : Set) โ (ยฌ (ยฌ A) โ A)) โ โฅ
-theorem3โ2โ2 p = {! !}
+theorem3โ2โ2 : ((A : Set) โ ยฌ ยฌ A โ A) โ โฅ
+theorem3โ2โ2 f = let wtf = f ๐ in {! !}
+ where
+ open axiom2โ10โ3
+
+ p : ๐ โก ๐
+ p = ua neg-equiv
+
+ wtf : ยฌ ยฌ ๐ โ ๐
+ wtf = f ๐
+
+ wtf2 : transport (ฮป A โ ยฌ ยฌ A โ A) p (f ๐) โก f ๐
+ wtf2 = apd f p
+
+ wtf3 : (u : ยฌ ยฌ ๐) โ transport (ฮป A โ ยฌ ยฌ A โ A) p (f ๐) u โก f ๐ u
+ wtf3 u = happly wtf2 u
+
+ wtf4 : (u : ยฌ ยฌ ๐) โ transport (ฮป A โ ยฌ ยฌ A โ A) p (f ๐) u โก transport (ฮป A โ A) p (f ๐ (transport (ฮป A โ ยฌ ยฌ A) (sym p) u))
+ wtf4 u =
+ let
+ wtf5 :
+ let A = ฮป A โ ยฌ ยฌ A in
+ let B = id in
+ transport (ฮป x โ A x โ B x) p (f ๐) โก ฮป x โ transport B p (f ๐ (transport A (sym p) x))
+ wtf5 = equation2โ9โ4 (f ๐) p
+ in
+ happly wtf5 u
+
+ wtf6 : (u v : ยฌ ยฌ ๐) โ u โก v
+ wtf6 u v = funext (ฮป x โ rec-โฅ (u x))
+
+ wtf7 : (u : ยฌ ยฌ ๐) โ transport (ฮป A โ ยฌ ยฌ A) (sym p) u โก u
+ wtf7 u = {! !}
+
+ wtf8 : (u : ยฌ ยฌ ๐) โ transport (ฮป A โ A) p (f ๐ u) โก f ๐ u
+ wtf8 u = {! sym (wtf3 u) !} โ sym (wtf4 u) โ wtf3 u
+
+ wtf9 : (u : ยฌ ยฌ ๐) โ neg (f ๐ u) โก f ๐ u
+ wtf9 = {! !}
+
+ wtf10 : (x : ๐) โ ยฌ (neg x โก x)
+ wtf10 true p = remark2โ12โ6 (sym p)
+ wtf10 false p = remark2โ12โ6 p
+
+ wtf11 : (u : ยฌ ยฌ ๐) โ ยฌ (neg (f ๐ u) โก (f ๐ u))
+ wtf11 u = wtf10 (f ๐ u)
+
+ wtf12 : (u : ยฌ ยฌ ๐) โ โฅ
+ wtf12 u = wtf11 u (wtf9 u)
```
### Corollary 3.2.7
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 8211f3f..3a0e4e3 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -47,8 +47,8 @@ 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 loop in
- {! !}
+ let wtf = lemma2โ3โ8 (ฮป x โ {! !}) loop in
+ {! !}
```
## 6.3 The interval
diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index b951e37..0e7f22c 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -7,6 +7,13 @@ open import HottBook.Chapter2
open import HottBook.Chapter6
```
+### Definition 8.0.1
+
+```
+ฯ : (n : โ) โ (A : Set) โ (a : A) โ Set
+
+```
+
## 8.1 ฯโ(Sยน)
### Definition 8.1.1