diff --git a/.vscode/settings.json b/.vscode/settings.json
index 1369c2f..41a3d0e 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,6 +1,6 @@
 {
 	"editor.unicodeHighlight.ambiguousCharacters": false,
-	"gitdoc.enabled": true,
+	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'"
 }
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index c23290d..612e516 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -78,9 +78,9 @@ data ⊥ : Set where
 ## 1.12 Identity types
 
 ```
+infix 4 _≡_
 data _≡_ {l} {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
-infix 4 _≡_
 ```
 
 ### 1.12.3 Disequality
@@ -99,3 +99,39 @@ J : {l₁ l₂ : Level} {A : Set l₁}
   → (x y : A) → (p : x ≡ y) → C x y p
 J C c x x refl = c x
 ```
+
+# Exercises
+
+## 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 : Set}
+  → (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 : Set}
+  → (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.
\ No newline at end of file
diff --git a/src/HottBook/Chapter1Exercises.lagda.md b/src/HottBook/Chapter1Exercises.lagda.md
deleted file mode 100644
index 85cd167..0000000
--- a/src/HottBook/Chapter1Exercises.lagda.md
+++ /dev/null
@@ -1,39 +0,0 @@
-```
-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.
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index ef2d98b..d0c5dc0 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -163,6 +163,7 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
 ### Definition 2.4.1 (Homotopy)
 
 ```
+infixl 18 _∼_
 _∼_ : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂}
   → (f g : (x : A) → P x)
   → Set (l₁ ⊔ l₂)
@@ -268,18 +269,18 @@ theorem2∙8∙1 x y = func x y , equiv x y
     rev : (x y : 𝟙) → 𝟙 → (x ≡ y)
     rev tt tt _ = refl
 
-    forward : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
-    forward tt tt refl = refl
-
-    backward : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
+    backward : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
     backward tt tt tt = refl
 
+    forward : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
+    forward tt tt refl = refl
+
     equiv : (x y : 𝟙) → isequiv (func x y)
     equiv x y = record
       { g = rev x y
-      ; g-id = forward x y
+      ; g-id = backward x y
       ; h = rev x y
-      ; h-id = backward x y
+      ; h-id = forward x y
       }
 ```
 
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 9ce17fb..67659e6 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -31,6 +31,24 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
 
 _Show that $(2 \simeq 2) \simeq 2$._
 
+lemma: equivalences are equal if their functions are equal
+
+```
+postulate
+  posEqLemma : {A B : Set}
+    → (e1 e2 : A ≃ B)
+    → (Σ.fst e1 ≡ Σ.fst e2)
+    → e1 ≡ e2
+
+eqLemma : {A B : Set}
+  → (e1 e2 : A ≃ B)
+  → (Σ.fst e1 ≡ Σ.fst e2)
+  → e1 ≡ e2
+eqLemma {A} {B} e1 e2 p = {!   !}
+```
+
+main proof:
+
 ```
 exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚
 exercise2∙13 = aux1 , equiv1
@@ -63,7 +81,10 @@ exercise2∙13 = aux1 , equiv1
 
     equiv1 : isequiv aux1
     g equiv1 = rev
-    g-id equiv1 e@(f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
+    g-id equiv1 true = refl
+    g-id equiv1 false = refl
+    h equiv1 = rev
+    h-id equiv1 e@(f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
       -- proving that given any equivalence e, that:
       --   ((aux1 ∘ rev) e ≡ id e)
       --   (rev (aux1 e) ≡ e)
@@ -74,43 +95,45 @@ exercise2∙13 = aux1 , equiv1
       --   - use function extensionality to show they behave the same
       --   - somehow use the fact that e.snd.g-id exists
       -- - snd (rev (e.fst true)) ≡ e.snd
-      Σ-≡ (funext test1 , {!   !})
+        -- test1 : (x : 𝟚) → fst (aux1 x) ≡ f x
+        -- test1 x with x , f true
+        -- test1 _ | true , true = {!  !}
+        -- test1 _ | true , false = {!  !}
+        -- test1 _ | false , y = {!   !}
+
+        -- equiv-funcs : (x : 𝟚) → aux1 x ≡ f x
+
+        -- -- if f mapped everything to the same value, then the inverse couldn't exist
+        -- -- how to state this as a proof?
+
+        -- asdf : (x : 𝟚) → neg (f x) ≡ f (neg x)
+        -- -- known that (f ∘ g) x ≡ x
+        -- -- g (f x) ≡ x
+        -- -- g (f true) ≡ true
+        -- -- maybe a proof by contradiction? suppose f true ≡ f false. why doesn't this work if f ∘ g ∼ id?
+        -- -- how to work backwards from the f ∘ g ∼ id? since we have a value `g-id` of that
+        -- asdf true = {!   !}
+        -- asdf false = {!   !}
+
+        -- ft = f true
+        -- ff = f false
+
+        -- div : ft ≢ ff
+        -- div p =
+        --   let
+        --     id𝟚 : 𝟚 → 𝟚
+        --     id𝟚 = id
+
+        --     wtf : ft ≡ ff
+        --     wtf = p
+
+        --     wtf2 : g ft ≡ g ff
+        --     wtf2 = ap g wtf
+
+        --   in {!   !}
+        -- in Σ-≡ (funext test1 , {!   !})
+      {!   !}
       where
-        test1 : (x : 𝟚) → fst (rev (f true)) x ≡ f x
-        test1 x with x , f true
-        test1 _ | true , true = {!  !}
-        test1 _ | true , false = {!  !}
-        test1 _ | false , y = {!   !}
-
-        -- if f mapped everything to the same value, then the inverse couldn't exist
-        -- how to state this as a proof?
-
-        asdf : (x : 𝟚) → neg (f x) ≡ f (neg x)
-        -- known that (f ∘ g) x ≡ x
-        -- g (f x) ≡ x
-        -- g (f true) ≡ true
-        -- maybe a proof by contradiction? suppose f true ≡ f false. why doesn't this work if f ∘ g ∼ id?
-        -- how to work backwards from the f ∘ g ∼ id? since we have a value `g-id` of that
-        asdf true = {!   !}
-        asdf false = {!   !}
-
-        ft = f true
-        ff = f false
-
-        div : ft ≢ ff
-        div p =
-          let
-            id𝟚 : 𝟚 → 𝟚
-            id𝟚 = id
-
-            wtf : ft ≡ ff
-            wtf = p
-
-            wtf2 : g ft ≡ g ff
-            wtf2 = ap g wtf
-
-          in {!   !}
-    h equiv1 = rev
-    h-id equiv1 true = refl
-    h-id equiv1 false = refl
+        test1 : (x : 𝟚 ≃ 𝟚) → aux1 x ≡ {!   !}
+        test1 (x , y) = {!  !}
 ```
diff --git a/src/HottBook/Chapter9.lagda.md b/src/HottBook/Chapter9.lagda.md
index adb71c8..7bada01 100644
--- a/src/HottBook/Chapter9.lagda.md
+++ b/src/HottBook/Chapter9.lagda.md
@@ -2,12 +2,36 @@
 module HottBook.Chapter9 where
 
 open import Agda.Primitive
+open import HottBook.Chapter1
 ```
 
 ## 9.1 Categories and precategories
 
 ```
-record precategory {l : Level} : Set (lsuc l) where
+record precat {l : Level} (A : Set l) : Set (lsuc l) where
   field
-    A : Set l
+    hom : (a b : A) → Set
+    id : (a : A) → hom a a
+    comp : {a b c : A} → hom a b → hom b c → hom a c
+    lol : (a b : A) → (f : hom a b) → (f ≡ comp f (id b)) × (f ≡ comp (id a) f)
+
+```
+
+### Definition 9.1.2
+
+```
+record isIso {l : Level} {A : Set l} {PC : precat A} {a b : A} (f : precat.hom PC a b) : Set (lsuc l) where
+  field
+    g : precat.hom PC b a
+    g-f : precat.comp f g ≡ precat.id a
+```
+
+### Lemma 9.1.4
+
+```
+idtoiso : {A : Set}
+  → (PC : precat A)
+  → (a b : A)
+  → a ≡ b
+  → precat.hom PC a b
 ```
\ No newline at end of file
diff --git a/src/HottBook/Util.agda b/src/HottBook/Util.agda
index 8ac1438..2d2c052 100644
--- a/src/HottBook/Util.agda
+++ b/src/HottBook/Util.agda
@@ -2,12 +2,5 @@ module HottBook.Util where
 
 open import Agda.Primitive
 
-infixl 40 _∘_
-_∘_ : {A B C : Set}
-  → (f : A → B)
-  → (g : B → C)
-  → A → C
-(f ∘ g) x = g (f x)
-
 id : {l : Level} {A : Set l} → A → A
 id x = x
\ No newline at end of file