diff --git a/src/2023-04-03-more-ch2.agda b/src/2023-04-03-more-ch2.agda
index cd1c462..d9b9ec8 100644
--- a/src/2023-04-03-more-ch2.agda
+++ b/src/2023-04-03-more-ch2.agda
@@ -1,8 +1,19 @@
 -- {{{
 
 open import Agda.Builtin.Equality
+open import Agda.Builtin.Sigma
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type)
 open import Data.Nat
+open import Data.Product
+open import Data.Product.Base
+open import Data.Product.Properties
+open import Data.Bool
+
+open import Data.Product using (_,_)
+open import Function.Base using (_∘_)
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Nullary.Negation.Core using (¬_)
 
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
@@ -71,6 +82,23 @@ apd {A} {B} f {x} {y} p =
   in
   path-ind D d x y p
 
+-- Fibers
+fiber : {A B : Type} → (f : A → B) → (y : B) → Type
+fiber {A} {B} f y = Σ[ x ∈ A ] f x ≡ y
+
+-- Contractibility
+isContr : Type → Type
+isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)
+
+-- Equivalence
+record isEquiv {A B : Type} (f : A → B) : Type where
+  field
+    equiv-proof : (y : B) → isContr (fiber f y)
+open isEquiv
+
+_≃_ : (A B : Type) → Type
+A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)
+
 -- }}}
 
 -------------------------------------------------------------------------------
@@ -101,20 +129,13 @@ l212-obv-proof-2 {A} x y z p q =
   in
   r x p
 
-l212-obv-proof-3 : {A : Type} → lemma-212
-l212-obv-proof-3 {A} x y z p q =
+l212-pairwise-1-2 : {A : Type} → (x y z : A) → (x ≡ y) → (y ≡ z)
+  → l212-obv-proof-1 ≡ l212-obv-proof-2
+l212-pairwise-1-2 {A} x y z p q =
   let
-    f : (y z : A) → (q : y ≡ z) → (x : A) → x ≡ y → x ≡ z
-    f = ?
-    r = f y z q
-
-    g : (x y : A) → (p : x ≡ y) → (x ≡ z)
-    g = path-ind
-      (λ a b a≡b → a ≡ z)
-      (λ a → r a ?)
-    s = g x y p
-  in
-  ?
+    left-proof = l212-obv-proof-1 x y z p q
+    right-proof = l212-obv-proof-2 x y z p q
+  in ?
 
 -- Exercise 2.3: Give a fourth, different proof of Lemma 2.1.2, and prove it
 -- equal to the others
@@ -132,9 +153,44 @@ l212-obv-proof-4 {A} x y z p q =
 -- Exercise 2.4: Define, by induction on n, a general notion of n-dimensional
 -- path in a type A, simultaneously with the type of boundaries of such paths
 
-data nPath {A : Type} : ℕ → Type where
-  zeroPath : (x y : A) → (p : x ≡ y) → nPath zero
-  sucPath : {n : ℕ} → (nPath n)
+-- p : (2 ≡ 1 + 1)
+-- p = refl
+--
+-- q : (2 ≡ 1 + 1)
+-- q = ?
+--
+-- p2 : p ≡ q
+-- q2 : p ≡ q
+--
+-- p3 : p2 ≡ q2
+--
+-- nSuc- npath 5
+
+-- data nPath {A : Type} : ℕ → Type where
+--   zeroPath : (x y : A) → (p : x ≡ y) → nPath zero
+--   sucPath : {n : ℕ}
+--     → (left : nPath n)
+--     → (right : nPath n)
+--     → (p : left ≡ right)
+--     → nPath (suc n)
+
+-- data nPath : (A : Type) → (x y : A) → Type where
+--   path-zero : (A : Type) → (x y : A) → (p : x ≡ y) → nPath A x y
+--   path-suc : (A : Type) → (x y : A)
+--     → (left : nPath A x y)
+--     → (right : nPath A x y)
+--     → (p : left ≡ right)
+--     → nPath (nPath A x y) left right
+
+data nPath : Type where
+
+-- p : nPath ℕ (1 + 1) 2
+-- p = path-zero ℕ (1 + 1) 2 refl
+-- 
+-- q : nPath ℕ (1 + 1) 2
+-- q = path-zero ℕ (1 + 1) 2 refl
+-- 
+-- p2 : nPath (nPath ℕ (1 + 1) 2) p q
 
 -- Exercise 2.5: Prove that the functions (2.3.6) and (2.3.7) are
 -- inverse-equivalences
@@ -153,7 +209,88 @@ f237 {p = p} {f = f} _ = ap f p
 -- Exercise 2.6: Prove that if p : x = y, then the function (p ∙ –) : (y = z) →
 -- (x = z) is an equivalence.
 
-e26 : {A : Type} {x y : A} → (p : x ≡ y) → ?
-
 -- Exercise 2.9. Prove that coproducts have the expected universal property,
 -- (A + B → X) ≃ (A → X) × (B → X).
+
+-- Exercise 2.13
+-- Show that (2 ≃ 2) ≃ 2
+
+-- The fiber of id for the Bool y (aka all x's such that id x ≡ y, which is just
+-- y)
+id-fiber-base : (y : Bool) → Σ[ x ∈ Bool ] id x ≡ y
+proj₁ (id-fiber-base y) = y
+proj₂ (id-fiber-base y) = refl
+
+id-fiber-is-contr : (y : Bool) → (y₁ : Σ[ x ∈ Bool ] id x ≡ y) → id-fiber-base y ≡ y₁
+id-fiber-is-contr y y₁ =
+  let
+    y₁-Bool-equiv = snd y₁
+
+    pair₁ : y ≡ fst y₁
+    pair₁ = sym y₁-Bool-equiv
+
+    snd-fiber : id (fst (id-fiber-base y)) ≡ y
+    snd-fiber = snd (id-fiber-base y)
+
+    pair₂ : subst (λ x → id x ≡ y) pair₁ (snd (id-fiber-base y)) ≡ snd y₁
+    pair₂ =
+      begin
+        subst (λ x → id x ≡ y) pair₁ snd-fiber
+      ≡⟨ ? ⟩
+        -- subst : Substitutive {A = A} _≡_ ℓ
+        -- subst P refl p = p
+        -- snd-fiber
+        ?
+      ≡⟨ ? ⟩
+        snd y₁
+      ∎
+
+    pair = pair₁ , pair₂
+  in Σ-≡,≡→≡ pair
+
+x : Substitutive ? ?
+x = ?
+
+-- Σ-≡,≡←≡ : p₁ ≡ p₂ → Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
+-- Σ-≡,≡←≡ refl = refl , refl
+
+-- A proof that for every y, the fiber of id for that y (which is just going to
+-- be y itself) is contractible, which means that for every pair of (a, path),
+-- there needs to be a path between that pair and the pair i gave above in id-fiber-base
+id-is-contr : (y : Bool) → isContr (fiber id y)
+proj₁ (id-is-contr y) = id-fiber-base y
+proj₂ (id-is-contr y) y₁ = id-fiber-is-contr y y₁
+
+id-is-eqv : isEquiv id
+id-is-eqv .equiv-proof y = ?
+
+id-eqv : Bool ≃ Bool
+proj₁ id-eqv = id
+proj₂ id-eqv = id-is-eqv
+
+-- proj₁ (proj₁ (proj₂ id-eqv .equiv-proof y)) = y
+-- proj₂ (proj₁ (proj₂ id-eqv .equiv-proof y)) = refl
+-- proj₂ (proj₂ id-eqv .equiv-proof y) y₁ = {! !}
+
+e213 : (Bool ≃ Bool) ≃ Bool
+
+e213-helper-1 : (y : Bool) → Σ (Bool ≃ Bool) (λ x → proj₁ e213 x ≡ y)
+proj₁ (e213-helper-1 y) = {! !}
+proj₂ (e213-helper-1 y) = {! !}
+
+proj₁ e213 bool-equiv = (proj₁ bool-equiv) true
+proj₁ (proj₂ e213 .equiv-proof y) = e213-helper-1 y
+proj₂ (proj₂ e213 .equiv-proof y) y₁ = {! !}
+
+
+
+
+
+
+
+
+
+
+
+
+ 
diff --git a/src/2023-05-06-equiv.lagda.md b/src/2023-05-06-equiv.lagda.md
new file mode 100644
index 0000000..8fcd82d
--- /dev/null
+++ b/src/2023-05-06-equiv.lagda.md
@@ -0,0 +1,130 @@
++++
+title = "Equivalences"
+slug = "equivalences"
+date = 2023-05-06
+tags = ["type-theory", "agda", "hott"]
+math = true
+draft = true
++++
+
+<details>
+  <summary>Imports</summary>
+
+```
+{-# OPTIONS --cubical #-}
+
+open import Agda.Primitive.Cubical
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+```
+
+</details>
+
+```
+Bool-id : Bool → Bool
+Bool-id true = true
+Bool-id false = false
+
+unap : {A B : Type} {x y : A} (f : A → B) → f x ≡ f y → x ≡ y
+unap p i = ?
+
+-- Need to convert point-wise equality into universally quantified equality?
+Bool-id-refl : (x : Bool) → (Bool-id x ≡ x)
+Bool-id-refl true = refl
+Bool-id-refl false = refl
+```
+
+The equivalence proof below involves the contractibility-of-fibers definition of
+an equivalence. There are others, but the "default" one used by the Cubical
+standard library uses this.
+
+```
+Bool-id-is-equiv : isEquiv Bool-id
+```
+
+In the contractibility-of-fibers proof, we must first establish our fibers. If
+we had $(f : A \rightarrow B)$, then this is saying given any $(y : B)$, we must
+provide:
+
+- an $(x : A)$ that would have gotten mapped to $y$ (preimage), and
+- a proof that $f\ x \equiv y$
+
+These are the two elements of the pair given below. Since our function is `id`,
+we can just give $y$ again, and use the `refl` function above for the equality
+proof
+
+```
+Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y
+```
+
+The next step is to prove that it's contractible. Using the same derivation for
+$y$ as above, this involves taking in another fiber $y_1$, and proving that it's
+equivalent the fiber we've just defined above.
+
+To prove fiber equality, we can just do point-wise equality over both the
+preimage of $y$, and then the second-level equality of the proof of $f\ x \equiv
+y$.
+
+In the first case here, we need to provide something that equals our $x$ above
+when $i = i0$, and something that equals the fiber $y_1$'s preimage $x_1$ when
+$i = i1$, aka $y \equiv proj_1\ y_1$.
+
+```
+Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst =
+  let
+    eqv = snd y₁
+    -- eqv : Bool-id (fst y₁) ≡ y
+
+    eqv2 = eqv ∙ sym (Bool-id-refl y)
+    -- eqv2 : Bool-id (fst y₁) ≡ Bool-id y
+
+    -- Ok, unap doesn't actually exist unless f is known to have an inverse.
+    -- Fortunately, because we're proving an equivalence, we know that f has an
+    -- inverse, in particular going from y to x, which in thise case is also y.
+    eqv3 = unap Bool-id eqv2
+
+    Bool-id-inv : Bool → Bool
+    Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst
+
+    eqv3′ = cong Bool-id-inv eqv2
+    give-me-info = ?
+    -- eqv3 : fst y₁ ≡ y
+
+    -- https://git.mzhang.io/school/cubical/issues/1
+    eqv4′ = ?
+    eqv4 = sym eqv3
+    -- eqv4 : y ≡ fst y₁
+  in
+  eqv4 i
+```
+
+Now we can prove that the path is the same
+
+\begin{CD}
+  A @> > > B \\\
+  @VVV @VVV \\\
+  C @> > > D
+\end{CD}
+
+- $A \rightarrow B$ is the path of the original fiber that we've specified, which is $f\ x \equiv y$
+- $C \rightarrow D$ is the path of the other fiber that we're proving, which is $proj_2\ y_1$
+
+So what we want now is `a-b ≡ c-d`
+
+```
+Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j =
+  let
+    a-b = Bool-id-refl y
+    c-d = y₁ .snd
+  in
+
+  -- https://git.mzhang.io/school/cubical/issues/2
+  ?
+```
+
+## Other Equivalences
+
+There are 2 other ways we can define equivalences:
+
+TODO: Talk about them being equivalent to each other
diff --git a/src/Simple.agda b/src/Simple.agda
index c9249a7..0fcedae 100644
--- a/src/Simple.agda
+++ b/src/Simple.agda
@@ -1,13 +1,15 @@
 {-# OPTIONS --cubical #-}
 
 open import Cubical.Foundations.Prelude 
-  using (_≡_; refl; _∙_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
+  using (_≡_; refl; _∙_; _∎; cong; sym; fst; snd; _,_; ~_)
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Foundations.Equiv using (isEquiv; equivProof; equiv-proof)
 open import Relation.Nullary using (¬_)
 open import Relation.Binary.Core using (Rel)
 open import Data.Nat
 
+open import Data.Bool
+
 sanity : 1 + 1 ≡ 2
 sanity = refl
 
@@ -38,3 +40,20 @@ sanity = refl
 -- _[_;_]′
 -- a [ 34 ; b ]
 --
+
+
+x : Bool
+x = true
+
+-- _&&_ : Bool → Bool → Bool
+
+-- (x && true) : Bool
+
+
+p : 2 + 3 ≡ 3 + 2
+p = refl
+
+-- _+_ : Nat → Nat → Nat
+-- zero  + m = m
+-- suc n + m = suc (n + m)
+p2 : (x y : ℕ) → x + y ≡ y + x