more

src/HottBook/Chapter1.lagda.md

@@ -14,6 +14,25 @@ open import Agda.Primitive
 
 ## 1.5 Product types
 
+```
+module Products where
+  data _×_ (A B : Set) : Set where
+    _,_ : A → B → A × B
+
+  pr₁ : {A B : Set} → A × B → A
+  pr₁ (a , _) = a
+
+  pr₂ : {A B : Set} → A × B → B
+  pr₂ (_ , b) = b
+
+  rec-× : {A B : Set}
+    → (C : Set)
+    → (A → B → C)
+    → A × B
+    → C
+  rec-× C f (a , b) = f a b
+```
+
 ```
 data 𝟙 : Set where
   tt : 𝟙
@@ -40,9 +59,31 @@ _×_ A B = Σ A (λ _ → B)
 ## 1.7 Coproduct types
 
 ```
--- infixl 6 _+_
--- _+_ : (A B : Set) → Set
--- A + B = A ⊎ B
+infixl 6 _+_
+data _+_ (A B : Set) : Set where
+  inl : A → A + B
+  inr : B → A + B
+```
+
+Recursor:
+
+```
+rec-+ : {A B : Set}
+  → (C : Set)
+  → (A → C)
+  → (B → C)
+  → A + B
+  → C
+rec-+ C f g (inl x) = f x
+rec-+ C f g (inr x) = g x
+```
+
+```
+
+data ⊥ : Set where
+
+rec-⊥ : (C : Set) → (x : ⊥) → C
+rec-⊥ C ()
 ```
 
 ## 1.8 The type of booleans
@@ -69,8 +110,6 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 ## 1.11 Propositions as types
 
 ```
-data ⊥ : Set where
-
 ¬_ : (A : Set) → Set
 ¬ A = A → ⊥
 ```

src/HottBook/Chapter1Exercises.lagda.md

@@ -0,0 +1,24 @@
+```
+module HottBook.Chapter1Exercises where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter1Util
+```
+
+### Exercise 1.1
+
+This can just be solved by expanding them. It's clear it results in the same expression.
+
+```
+exercise1∙1 : {A B C D : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → (h : C → D)
+  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
+exercise1∙1 f g h = refl
+```
+
+### Exercise 1.2
+
+```
+```

src/HottBook/Chapter2.lagda.md

@@ -307,18 +307,18 @@ theorem2∙8∙1 x y = func x y , equiv x y
     rev : (x y : 𝟙) → 𝟙 → (x ≡ y)
     rev tt tt _ = refl
 
-    backward : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
-    backward tt tt tt = refl
+    backwards : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
+    backwards tt tt tt = refl
 
-    forward : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
-    forward tt tt refl = refl
+    forwards : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
+    forwards tt tt refl = refl
 
     equiv : (x y : 𝟙) → isequiv (func x y)
     equiv x y = record
       { g = rev x y
-      ; g-id = backward x y
+      ; g-id = backwards x y
       ; h = rev x y
-      ; h-id = forward x y
+      ; h-id = forwards x y
       }
 ```
 

src/HottBook/Chapter2Exercises.lagda.md

@@ -44,7 +44,6 @@ postulate
     → (Σ.fst e1 ≡ Σ.fst e2)
     → e1 ≡ e2
 
-
 -- What the hell
 -- https://agda.readthedocs.io/en/v2.6.1/language/with-abstraction.html#the-inspect-idiom
 module Wtf {a b} {A : Set a} {B : A → Set b} where

src/HottBook/Chapter3.lagda.md

@@ -1,7 +1,11 @@
 ```
 module HottBook.Chapter3 where
 
+open import Agda.Primitive
 open import HottBook.Chapter1
+open import HottBook.Chapter1Util
+open import HottBook.Chapter2
+open import HottBook.Util
 
 ```
 
@@ -10,7 +14,7 @@ open import HottBook.Chapter1
 ### Definition 3.1.1
 
 ```
-isSet : (A : Set) → Set
+isSet : {l : Level} (A : Set l) → Set l
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
@@ -31,12 +35,40 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.4
 
 ```
-ℕ-is-Set : isSet ℕ
-ℕ-is-Set = {!   !}
+-- ℕ-is-Set : isSet ℕ
+-- ℕ-is-Set = 
 ```
 
 ## 3.2 Propositions as types?
 
+## 3.3 Mere propositions
+
+### Definition 3.3.1
+
+```
+isProp : (P : Set) → Set
+isProp P = (x y : P) → x ≡ y
+```
+
+### Lemma 3.3.2
+
+```
+lemma3∙2∙2 : {P : Set}
+  → isProp P
+  → (x₀ : P)
+  → P ≃ 𝟙
+lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
+  where
+    f : P → 𝟙
+    f x = tt
+
+    g : 𝟙 → P
+    g u = x₀
+
+    forwards : f ∘ g ∼ id
+    forwards x = {! refl  !}
+```
+
 ## 3.4 Classical vs. intuitionistic logic
 
 ### Definition 3.4.3

src/HottBook/Chapter3Exercises.lagda.md

@@ -0,0 +1,20 @@
+```
+module HottBook.Chapter3Exercises where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3
+```
+
+### Exercise 3.1
+
+ProvethatifA≃BandAisaset,thensoisB.
+
+```
+exercise3∙1 : {A B : Set}
+  → isSet (A ≃ B)
+  → isSet A
+  → isSet B
+exercise3∙1 {A} {B} isSetAB isSetA xB yB pB qB =
+  {!   !}
+```

src/HottBook/Chapter6.lagda.md

@@ -57,4 +57,13 @@ postulate
   0I : I
   1I : I
   seg : 0I ≡ 1I
+```
+
+## 6.10 Quotients
+
+```
+module Quotient (A : Set) (R : A × A → Prop) where
+  postulate
+    _/_ : Set → Set → Set
+    q : (A : Set) → A / A
 ```