some more shit

src/HottBook/Chapter1Exercises.lagda.md

@@ -0,0 +1,39 @@
+```
+module HottBook.Chapter1Exercises where
+
+open import Relation.Binary.PropositionalEquality as Eq
+open Eq
+open Eq.≡-Reasoning
+Type = Set
+
+infixl 6 _∙_
+_∙_ = trans
+```
+
+### Exercise 1.1
+
+Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C.
+Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f.
+
+```
+composite : {A B C : Type} → (f : A → B) → (g : B → C) → A → C
+composite f g x = g (f x)
+
+syntax composite f g = g ∘ f
+
+composite-assoc : {A B C D : Type} → (f : A → B) → (g : B → C) → (h : C → D)
+  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
+composite-assoc f g h = refl
+```
+
+### Exercise 1.2
+
+### Exercise 1.14
+
+Why do the induction principles for identity types not allow us to construct a
+function f : ∏(x:A) ∏(p:x=x)(p = refl_x) with the defining equation f (x,
+refl_x) :≡ refl_(refl_x) ?
+
+Under non-UIP systems, there are identity types that are different from refl,
+and this ability gives us higher dimensional paths. Otherwise, we would be
+dealing with propositions only.

src/HottBook/Chapter2.lagda.md

@@ -6,6 +6,8 @@ open import Function
 open import Data.Product
 open import Data.Product.Properties
 Type = Set
+
+infixr 6 _∙_
 _∙_ = trans
 ```
 
@@ -133,3 +135,107 @@ lemma2311 {A} {P} {Q} f {x} {y} p u =
 ```
 
 ## 2.4 Homotopies and equivalences
+
+### Definition 2.4.1 (Homotopy)
+
+```
+_∼_ : {A : Type} {P : A → Type} (f g : (x : A) → P x) → Type
+_∼_ {A} f g = (x : A) → f x ≡ g x
+```
+
+### Lemma 2.4.2
+
+Homotopy forms an equivalence:
+
+```
+∼-refl : {A : Type} {P : A → Type} (f : (x : A) → P x) → f ∼ f
+∼-refl f x = refl
+
+∼-sym : {A : Type} {P : A → Type} (f g : (x : A) → P x) → f ∼ g → g ∼ f
+∼-sym f g f∼g x = sym (f∼g x)
+
+∼-trans : {A : Type} {P : A → Type} (f g h : (x : A) → P x)
+  → f ∼ g → g ∼ h → f ∼ h
+∼-trans f g h f∼g g∼h x = f∼g x ∙ g∼h x
+```
+
+### Lemma 2.4.3
+
+```
+-- lemma243 : {A B : Type} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y)
+--   → H x ∙ ap g p ≡ ap f p ∙ H y
+-- lemma243 {f} {g} H {x} {y} p =
+--   J (λ the what → (H x ∙ ? ≡ ? ∙ H the)) p ?
+```
+
+### Definition 2.4.6
+
+```
+record qinv {A B : Type} (f : A → B) : Type where
+  field
+    g : B → A
+    α : (f ∘ g) ∼ id
+    β : (g ∘ f) ∼ id
+```
+
+### Example 2.4.7
+
+```
+id-qinv : qinv id
+id-qinv = record
+  { g = id
+  ; α = λ _ → refl
+  ; β = λ _ → refl
+  }
+```
+
+## 2.8 The unit type
+
+```
+data 𝟙 : Set where
+  ⋆ : 𝟙
+```
+
+### Theorem 2.8.1
+
+```
+-- open import Function.HalfAdjointEquivalence
+-- _is-⋆ : (x : 𝟙) → x ≡ ⋆
+-- ⋆ is-⋆ = refl
+-- 
+-- theorem281-helper2 : {x : 𝟙} → (p : x ≡ x) → p ≡ refl
+-- theorem281-helper2 {x} p = 
+--   let a = sym (x is-⋆) ∙ p ∙ (x is-⋆) in
+--   J (λ the what → p ≡ the) ? ?
+-- 
+-- theorem281-helper : {x y : 𝟙} → (p : x ≡ y) → (x is-⋆) ∙ sym (y is-⋆) ≡ p
+-- theorem281-helper {x} p =
+--   J (λ the what → (x is-⋆) ∙ sym (the is-⋆) ≡ what) p (theorem281-helper2 _)
+-- 
+-- theorem281 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
+-- theorem281 x y = record
+--   { to = λ _ → ⋆
+--   ; from = λ _ → (x is-⋆) ∙ sym (y is-⋆)
+--   ; left-inverse-of = theorem281-helper
+--   -- λ z → J (λ the what → (x is-⋆) ∙ sym (the is-⋆) ≡ what) z ?
+--   ; right-inverse-of = λ z → sym (z is-⋆)
+--   ; left-right = ?
+--   }
+```
+
+## 2.9 Π-types and the function extensionality axiom
+
+### Lemma 2.9.2
+
+```
+happly : {A B : Type} → (f g : A → B) → {x : A} → (p : f ≡ g) → f x ≡ g x
+happly f g {x} p =
+  J (λ the what → f x ≡ the x) p refl
+```
+
+### Axiom 2.9.3 (Function extensionality)
+
+```
+postulate
+  funext : {A B : Type} → (f g : A → B) → {x : A} → (p : f x ≡ g x) → f ≡ g
+```

src/HottBook/Chapter4.lagda.md

@@ -0,0 +1,9 @@
+```
+module HottBook.Chapter4 where
+```
+
+## 4.1 Quasi-inverses
+
+```
+-- qinv : {A B : Type} (f : A → B) → 
+```