diff --git a/bidir/bidir.ts b/bidir/bidir.ts
new file mode 100644
index 0000000..07a0319
--- /dev/null
+++ b/bidir/bidir.ts
@@ -0,0 +1,57 @@
+import { isTypeInContext } from "./contexts";
+import { ContextEntry, Term, Type } from "./data";
+
+function check(
+  ctx: ContextEntry[],
+  term: Term,
+  type: Type
+): [boolean, ContextEntry[]] {
+  switch (term.kind) {
+    case "var":
+      break;
+    case "unit":
+      return [type.kind === "unit", ctx];
+    case "lambda": {
+      // Get A and B first
+      if (type.kind !== "arrow") return [false, ctx];
+      const { input: A, output: B } = type;
+    }
+    case "app":
+      break;
+    case "annot":
+      break;
+  }
+}
+
+function synthesize(ctx: ContextEntry[], term: Term): [Type, ContextEntry[]] {
+  switch (term.kind) {
+    case "var": {
+      const res = lookupTypeVariable(ctx, term.name);
+      if (!res) throw new Error("wtf?");
+      return [res, ctx];
+    }
+    case "unit":
+      return [{ kind: "unit" }, ctx];
+    case "lambda": {
+    }
+    case "app":
+      break;
+    case "annot": {
+      // Require that the type exists
+      if (!isTypeInContext(term.type, ctx))
+        throw new Error("type doesn't exist");
+
+      // Require that the term checks against the type
+      const [result, outputCtx] = check(ctx, term.term, term.type);
+      if (!result) throw new Error("invalid annotation: term doesn't check");
+
+      return [term.type, outputCtx];
+    }
+  }
+}
+
+function synthesizeApp(
+  ctx: ContextEntry[],
+  funcType: Type,
+  term: Term
+): [Type, ContextEntry[]] {}
diff --git a/bidir/contexts.ts b/bidir/contexts.ts
new file mode 100644
index 0000000..aa57188
--- /dev/null
+++ b/bidir/contexts.ts
@@ -0,0 +1,18 @@
+// Helper functions for dealing with contexts
+
+import { ContextEntry, Type } from "./data";
+import { isEqual } from "lodash";
+
+/** Γ |- A (is the given type in this context?) */
+export function isTypeInContext(type: Type, ctx: ContextEntry[]): boolean {
+  for (const entry of ctx) {
+    switch (entry.kind) {
+      case "termAnnot":
+        if (isEqual(entry.type, type)) return true;
+        break;
+      default:
+        continue;
+    }
+  }
+  return false;
+}
diff --git a/bidir/data.ts b/bidir/data.ts
new file mode 100644
index 0000000..276a26d
--- /dev/null
+++ b/bidir/data.ts
@@ -0,0 +1,42 @@
+/**
+ * Terms e ::= x | () | λx. e | e e | (e : A)
+ * Types A, B, C ::= 1 | α | ^α | ∀α. A | A → B
+ * Monotypes τ, σ ::= 1 | α | ^α | τ → σ
+ * Contexts Γ, ∆, Θ ::= · | Γ, α | Γ, x : A
+ *                      | Γ, ^α | Γ, ^α = τ | Γ, I^α
+ * Complete Contexts Ω ::= · | Ω, α | Ω, x : A
+ *                      | Ω, ^α = τ | Ω, I^
+ */
+
+export type Term =
+  | { kind: "var"; name: string }
+  | { kind: "unit" }
+  | { kind: "lambda"; name: string; body: Term }
+  | { kind: "app"; func: Term; arg: Term }
+  | { kind: "annot"; term: Term; type: Type };
+
+export type Type =
+  | { kind: "unit" }
+  | { kind: "var"; name: string }
+  | { kind: "existential"; name: string }
+  | { kind: "poly"; name: string; type: Type }
+  | { kind: "arrow"; input: Type; output: Type };
+
+export type Monotype =
+  | { kind: "unit" }
+  | { kind: "var"; name: string }
+  | { kind: "existential"; name: string }
+  | { kind: "arrow"; input: Monotype; output: Monotype };
+
+export type ContextEntry =
+  | { kind: "typeVar"; name: string }
+  | { kind: "termAnnot"; name: string; type: Type }
+  | { kind: "existentialVar"; name: string }
+  | { kind: "existentialSolved"; name: string; type: Monotype }
+  | { kind: "marker"; name: string };
+
+export type CompleteContextEntry =
+  | { kind: "typeVar"; name: string }
+  | { kind: "termAnnot"; name: string; type: Type }
+  | { kind: "existentialSolved"; name: string; type: Monotype }
+  | { kind: "marker"; name: string };
diff --git a/extraexercises.agda b/extraexercises.agda
new file mode 100644
index 0000000..caa831e
--- /dev/null
+++ b/extraexercises.agda
@@ -0,0 +1,5 @@
+module extraexercises where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality as Eq
+open Eq.≡-Reasoning
diff --git a/hwk1.typ b/hwk1.typ
index 4750b59..537c520 100644
--- a/hwk1.typ
+++ b/hwk1.typ
@@ -1,26 +1,36 @@
+#set document(title: "Homework 1", author: "Michael Zhang <zhan4854@umn.edu>")
 #set page("us-letter")
 #import "@preview/prooftrees:0.1.0": *
 
+= Homework 1
+
+Michael Zhang \<zhan4854\@umn.edu\>
+
+
 #let c(body) = {
   set text(gray)
   body
 }
 
-= Problem 1
+$#math.op("f")\(x)$
+
+== Problem 1
+
+$top : "Set"$
+
+$"case"_top$
 
 #c[Define `funsplit` in terms of `apply`.]
 
-$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $
+$ "funsplit"(f, d) &equiv d((x) "apply"(f, x)) $
 
 In the case of $f = lambda b$ the following evaluation occurs:
 
-$ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \
-&equiv d(((x)x)(b)) \
+$ "funsplit"(lambda b, d) &equiv d((x) "apply"(lambda b, x)) \
+&equiv d((x) (b(x))) \
 &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
+== Problem 2
 
 #c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:
 
@@ -91,112 +101,115 @@ $ #tree(
 ) $
 
 $ #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]$],
+  axi[$x in NN$],
+  axi[$y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
+  bin(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN$],
+  uni(right_label: "(3)")[$"suc"("natrec"(x, 0, (u, v) "suc"(v))) = "suc"(x) in NN$],
+  uni(right_label: "natrec")[$"natrec"("suc"(x), 0, (u, v) "suc"(v))) = "suc"(x) in NN$],
 ) $
   
-$ #tree(
+$ #pad(left: -4em, 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)$],
-) $
+  uni(right_label: "(7, 9, 10)")[$"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: "(5, 11)")[$"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()
+// #pagebreak()
 
-Then, we can use this:
+// Then, we can use this:
 
-#set math.equation(numbering: none)
+// #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)$],
-)
+// #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:
+// 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$],
-)
+// #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:
+// 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))$],
-)
+// #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:
+// 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))$],
-)
+// #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:
+// 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[$"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[$"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]$],
-)
+// #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()
+// ---
+// #pagebreak()
 
-#{
-  let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
+// #{
+//   let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
 
-  tree(
-    axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
-    uni[$split1 equiv x in NN [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, 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[$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[$plus.circle(x, 0) equiv split1 [x in NN]$],
+//   )
 
-  tree(
-    axi[$split1 equiv x [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
+//   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