diff --git a/.gitignore b/.gitignore
index 938fec3..3618313 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 .DS_Store
 *.pdf
+
+_build
\ No newline at end of file
diff --git a/csci8980-f23.agda-lib b/csci8980-f23.agda-lib
index 4e12c2b..6017a53 100644
--- a/csci8980-f23.agda-lib
+++ b/csci8980-f23.agda-lib
@@ -1,2 +1,2 @@
-include: bidir
+include: . bidir
 depend: standard-library
\ No newline at end of file
diff --git a/hwk1.agda b/hwk1.agda
new file mode 100644
index 0000000..8453996
--- /dev/null
+++ b/hwk1.agda
@@ -0,0 +1,29 @@
+module hwk1 where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality as Eq
+open Eq.≡-Reasoning
+
+natrec : {C : Set} → (a : ℕ) → (d : C) → (e : ℕ → C → C) → C
+natrec zero d e = d
+natrec (suc b) d e = e b (natrec b d e)
+
+⊕ : ℕ → ℕ → ℕ
+⊕ x y = natrec x y (λ u v → suc v)
+
+problem2-lemma : (x : ℕ) → natrec x 0 (λ u v → suc v) ≡ x
+problem2-lemma zero = refl
+problem2-lemma (suc x) = cong suc (problem2-lemma x)
+
+-- (λ u v → suc v) x (natrec x 0 (λ u v → suc v))
+-- suc (natrec x 0 (λ u v → suc v))
+ 
+problem2 : (x : ℕ) → ⊕ x 0 ≡ x
+problem2 x = problem2-lemma x
+--   begin
+--     ⊕ x 0
+--   ≡⟨⟩
+--     natrec x 0 (λ u v → suc v)
+--   ≡⟨ {!   !} ⟩
+--     x
+--   ∎
\ No newline at end of file
diff --git a/hwk1.typ b/hwk1.typ
index 58abf60..4750b59 100644
--- a/hwk1.typ
+++ b/hwk1.typ
@@ -1,11 +1,14 @@
+#set page("us-letter")
 #import "@preview/prooftrees:0.1.0": *
 
-#let natrec = text[natrec]
-#let suc = text[suc]
+#let c(body) = {
+  set text(gray)
+  body
+}
 
 = Problem 1
 
-Define `funsplit` in terms of `apply`.
+#c[Define `funsplit` in terms of `apply`.]
 
 $ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $
 
@@ -15,27 +18,185 @@ $ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \
 &equiv d(((x)x)(b)) \
 &equiv d(b) $
 
+NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$?
+
 = Problem 2
 
-Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:
+#c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:
 
 $ plus.circle(x, 0) = x ∈ NN [x ∈ NN] $
 
-Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.
+Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.]
+
+#set math.equation(numbering: "(1)")
+
+First, let me reprint some rules from the textbook here to refer to them more easily from here on:
+
+- Reflexivity (pg. 37 in textbook)
+
+  $ #tree(axi[$a in A$], uni[$a = a in A$]) $
+
+- Propositions as sets (pg. 37 in textbook)
+
+  $ #tree(axi[$a∈A$], uni[$A "true"$]) $
+
+- Substitution in elements from chapter 5 (pg. 38 in textbook)
+
+  $ #tree(
+    axi[$c(x) in C(x) [x in A]$],
+    axi[$a = b in A$],
+    bin[$c(a) = c(b) in C(a)$],
+  ) $
+
+- Eq-introduction rule (pg. 60 in textbook)
+
+  $ #tree(axi[$a = b in A$], uni[$"eq" in "Eq"(A, a, b)$]) $
+
+- Strong Eq-elimination (pg. 61 in textbook)
+
+  $ #tree(axi[$c ∈ "Eq"(A, a, b)$], uni[$a=b∈A$]) $
+
+- N-introduction (pg. 63 in textbook)
+
+  $ #tree(axi[$a in NN$], uni[$"suc"(a) in NN$]) $
+
+- Nat rec (pg. 64 in textbook)
+
+  $ #tree(
+    axi[$a in NN$],
+    axi[$C(v) "set" [v in NN]$],
+    axi[$d in C(0)$],
+    axi[$e(x, y) in C("suc"(x)) [x in NN, y in C(x)]$],
+    nary(4)[$"natrec"(a, d, e) in C(a)$],
+  ) $
+
+
+- Peano's 5th axiom (pg. 65 in textbook)
+
+  $ #tree(
+    axi[$a ∈ NN$],
+    axi[$C(v) "prop" [v ∈ N]$],
+    axi[$C(0) "true"$],
+    axi[$C("suc"(x)) "true" [C(x) "true"]$],
+    nary(4)[$C(a) "true"$]
+  ) $
+
+I can now form the derivation:
+
+$ #tree(
+  axi[$0 in NN$],
+  uni(right_label: "(1)")[$0 = 0 in NN$],
+  uni(right_label: "natrec")[$"natrec"(0, 0, (u, v) "suc"(v)) = 0 in NN$],
+  uni(right_label: "(4)")[$"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$],
+) $
+
+$ #tree(
+  axi[$x = y in NN [x in NN, y in NN]$],
+  uni(right_label: "(3, 6)")[$"suc"(x) = "suc"(y) in NN [x in NN, y in NN]$],
+) $
+  
+$ #tree(
+  axi(pad(bottom: .2em, [
+    $x in NN$ \
+    $"Eq"(NN, "natrec"(n, 0, (u, v) "suc"(v)), n) "set" [n in NN]$ \
+    $"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$ \
+    $"eq"_"suc" (x, y) in "Eq"(NN, "natrec"("suc"(x), 0, (u, v) "suc"(v)), "suc"(x)) [x in NN, y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)]$ \
+  ])),
+  uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
+) $
+
+#tree(
+  axi[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
+  uni(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
+  uni(right_label: [#sym.plus.circle])[$plus.circle(x, 0) = x in NN [x in NN]$],
+)
+
+#pagebreak()
+
+Then, we can use this:
+
+#set math.equation(numbering: none)
+
+#tree(
+  axi[$0 in NN$],
+  uni(right_label: "(1)")[$0 = 0 in NN$],
+  uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
+)
+
+Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:
+
+#tree(
+  axi[$"suc"(x) in C(x) [x in NN]$],
+  axi[$x = y in NN$],
+  bin[$"suc"(x) = "suc"(y) in NN$],
+)
+
+Then, convert this to Eq:
+
+#tree(
+  axi[$"suc"(x) = "suc"(y) in NN$],
+  axi[$x = y in NN$],
+  bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
+)
+
+We can form a lambda term over eq objects using $lambda$-introduction:
+
+#tree(
+  axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
+  uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
+)
+
+This gives us what we need to perform induction over nats:
+
+#tree(
+  axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
+  uni[]
+)
+
+#tree(
+  axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
+  uni[],
+)
+
+#tree(
+  axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
+  uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
+  uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
+)
+
+---
+#pagebreak()
 
 #{
-    tree(
-        axi[$C(v) "set" [v in NN]$],
-        axi[$x in NN$],
-        axi[$d in C(0)$],
-        axi[$x in NN$],
-        nary(4)[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
-    )
+  let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
 
-    tree(
-        axi[],
-        uni[$plus.circle(x, 0) equiv natrec(x, 0, (u, v) suc(v)) [Gamma tack.r x in NN]$],
-        axi[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
-        bin[$plus.circle(x, 0) equiv x in NN [(Gamma, Delta) tack.r x in NN]$],
-    )
+  tree(
+    axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
+    uni[$split1 equiv x in NN [x in NN]$],
+  )
+
+  tree(
+    // axi[$c in "Eq"(NN, split1, 0), x)$],
+    axi[$split1 equiv x in NN [x in NN]$],
+    uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
+  )
+
+  tree(
+    axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
+    uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
+  )
+
+  tree(
+    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
+  )
+
+  tree(
+    axi[$split1 equiv x [x in NN]$],
+  )
+
+  tree(
+    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
+    axi[$split1 equiv x [x in NN]$],
+    bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
+  )
 }
\ No newline at end of file