diff --git a/README.md b/README.md
index 16490c37c..88dfc0497 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,8 @@
 # Kind-Core
 
-Kind is a very raw and minimal Type Theory.
+Kind is a minimal Proof Checker.
+
+Example files on [https://github.com/HigherOrderCO/MonoBook](HigherOrderCO/MonoBook).
 
 # Usage
 
diff --git a/book/Bool/Type.kind b/book/Bool/Type.kind
deleted file mode 100644
index e0bf623d9..000000000
--- a/book/Bool/Type.kind
+++ /dev/null
@@ -1,5 +0,0 @@
-// Defines the Boolean type with two constructors: true and false.
-Bool : * = #[]{
-  #t{} : Bool
-  #f{} : Bool
-}
diff --git a/book/Bool/and.kind b/book/Bool/and.kind
deleted file mode 100644
index 63718dcfa..000000000
--- a/book/Bool/and.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// Performs logical AND operation on two boolean values.
-// - a: The first boolean value.
-// - b: The second boolean value.
-// = True if both 'a' and 'b' are true, false otherwise.
-Bool/and
-: ∀(a: Bool)
-  ∀(b: Bool)
-  Bool
-= λ{
-  #t: λb b
-  #f: λb #f{}
-}
diff --git a/book/Bool/if.kind b/book/Bool/if.kind
deleted file mode 100644
index f7ab0f2c0..000000000
--- a/book/Bool/if.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-Bool/if
-: ∀(b: Bool)
-  ∀(P: *)
-  ∀(t: P)
-  ∀(f: P)
-  P
-= λ{
-  #t: λP λt λf t
-  #f: λP λt λf f
-}
diff --git a/book/Bool/match.kind b/book/Bool/match.kind
deleted file mode 100644
index 537778f73..000000000
--- a/book/Bool/match.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-Bool/match
-: ∀(P: ∀(x: Bool) *)
-  ∀(t: (P #t{}))
-  ∀(f: (P #f{}))
-  ∀(b: Bool)
-  (P b)
-= λP λt λf λ{
-  #t: t
-  #f: f
-}
diff --git a/book/Bool/not.kind b/book/Bool/not.kind
deleted file mode 100644
index 21d882eee..000000000
--- a/book/Bool/not.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-// Performs logical NOT operation on a boolean value.
-// - a: The boolean value to negate.
-// = True if 'a' is false, false if 'a' is true.
-Bool/not
-: ∀(a: Bool)
-  Bool
-= λ{
-  #t: #f{}
-  #f: #t{}
-}
diff --git a/book/Bool/or.kind b/book/Bool/or.kind
deleted file mode 100644
index 617c42882..000000000
--- a/book/Bool/or.kind
+++ /dev/null
@@ -1,14 +0,0 @@
-// Performs logical OR operation on two boolean values.
-// - a: The first boolean value.
-// - b: The second boolean value.
-// = True if either 'a' or 'b' (or both) are true, false otherwise.
-Bool/or
-: ∀(a: Bool)
-  ∀(b: Bool)
-  Bool
-= λ{
-  #t: λb
-    #t{}
-  #f: λb
-    b
-}
diff --git a/book/Bool/xor.kind b/book/Bool/xor.kind
deleted file mode 100644
index 07a55d2cd..000000000
--- a/book/Bool/xor.kind
+++ /dev/null
@@ -1,14 +0,0 @@
-// Performs logical XOR (exclusive or) operation on two boolean values.
-// - a: The first boolean value.
-// - b: The second boolean value.
-// = True if 'a' and 'b' are different, false if they are the same.
-Bool/xor
-: ∀(a: Bool)
-  ∀(b: Bool)
-  Bool
-= λ{
-  #t: λb
-    (Bool/not b)
-  #f: λb
-    b
-}
diff --git a/book/Equal.kind b/book/Equal.kind
deleted file mode 100644
index 6f7a0a37d..000000000
--- a/book/Equal.kind
+++ /dev/null
@@ -1,14 +0,0 @@
-// Defines propositional equality between two values of the same type.
-// - A: The type of the values being compared.
-// - a: The first value.
-// - b: The second value.
-// Constructor:
-// - refl: Represents reflexivity, i.e., that `a` equals itself.
-Equal
-: ∀(A: *)
-  ∀(a: A)
-  ∀(b: A)
-  *
-= λA λa λb #[a b]{
-  #refl{} : (Equal A a a)
-}
diff --git a/book/Equal/apply.kind b/book/Equal/apply.kind
deleted file mode 100644
index 99ddbef3f..000000000
--- a/book/Equal/apply.kind
+++ /dev/null
@@ -1,19 +0,0 @@
-// Applies a function to both sides of an equality proof.
-// - A: The type of the compared values.
-// - B: The type of the compared values after applying the function.
-// - a: The first compared value.
-// - b: The second compared value.
-// - f: The function to apply to both sides of the equality.
-// - e: The proof of equality between `a` and `b`.
-// = A proof that `(f a)` is equal to `(f b)`.
-Equal/apply
-: ∀(A: *)
-  ∀(B: *)
-  ∀(a: A)
-  ∀(b: A)
-  ∀(f: ∀(x: A) B)
-  ∀(e: (Equal A a b))
-  (Equal B (f a) (f b))
-= λA λB λa λb λf λ{
-  #refl: #refl{}
-}
diff --git a/book/Equal/refl.kind b/book/Equal/refl.kind
deleted file mode 100644
index d62c19db9..000000000
--- a/book/Equal/refl.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-// Constructs a proof of reflexivity for propositional equality.
-// - A: The type of the value.
-// - x: The value for which to construct the reflexivity proof.
-// = A proof that `x` is equal to itself.
-Equal/refl
-: ∀(A: *)
-  ∀(x: A)
-  (Equal A x x)
-= λA λx
-  #refl{}
diff --git a/book/Equal/rewrite.kind b/book/Equal/rewrite.kind
deleted file mode 100644
index c999bf8e3..000000000
--- a/book/Equal/rewrite.kind
+++ /dev/null
@@ -1,19 +0,0 @@
-// Rewrites a proof using an equality.
-// - T: The type of the values being compared.
-// - a: The first value.
-// - b: The second value.
-// - e: The proof of equality between `a` and `b`.
-// - P: A predicate that depends on a value of type T.
-// - x: A proof of (P a).
-// = A proof of (P b), obtained by rewriting `x` using the equality `e`.
-Equal/rewrite
-: ∀(T: *)
-  ∀(a: T)
-  ∀(b: T)
-  ∀(e: (Equal T a b))
-  ∀(P: ∀(x: T) *)
-  ∀(x: (P a))
-  (P b)
-= λT λa λb λ{
-  #refl: λP λx x
-}
diff --git a/book/List.kind b/book/List.kind
deleted file mode 100644
index b1aee730e..000000000
--- a/book/List.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// Defines a generic list datatype.
-// - A: The type of elements in the list.
-// Constructors:
-// - nil: Represents an empty list.
-// - con: Adds an element to the front of a list.
-List
-: ∀(A: *)
-  *
-= λA #[]{
-  #nil{} : (List A)
-  #con{ head:A tail:(List A) } : (List A)
-}
diff --git a/book/List/con.kind b/book/List/con.kind
deleted file mode 100644
index 465a3bc38..000000000
--- a/book/List/con.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// Constructs a new list by adding an element to the front of an existing list.
-// - A: The type of elements in the list.
-// - head: The element to add to the front of the list.
-// - tail: The current list.
-// = A new list with `head` as its 1st element, followed by the elements of `tail`.
-List/con
-: ∀(A: *)
-  ∀(head: A)
-  ∀(tail: (List A))
-  (List A)
-= λA λhead λtail
-  #con{head tail}
diff --git a/book/List/filter.kind b/book/List/filter.kind
deleted file mode 100644
index 24e8e9951..000000000
--- a/book/List/filter.kind
+++ /dev/null
@@ -1,16 +0,0 @@
-// Filters a list, keeping only elements that satisfy a given predicate.
-// - A: The type of elements in the list.
-// - xs: The input list.
-// - pred: The predicate function to apply to each element.
-// = A new list containing only the elements of `xs` that satisfy `pred`.
-List/filter
-: ∀(A: *)
-  ∀(xs: (List A))
-  ∀(fn: ∀(x: A) Bool)
-  (List A)
-= λA λ{
-  #nil: λfn
-    #nil{}
-  #con: λxs.head λxs.tail λfn
-    (List/filter/go A (fn xs.head) xs.head xs.tail fn)
-}
diff --git a/book/List/filter/go.kind b/book/List/filter/go.kind
deleted file mode 100644
index f637549aa..000000000
--- a/book/List/filter/go.kind
+++ /dev/null
@@ -1,20 +0,0 @@
-// Helper function for List/filter that decides whether to include the current element.
-// - A: The type of elements in the list.
-// - cond: The result of applying the predicate to the current element.
-// - head: The current element being considered.
-// - tail: The rest of the list to be filtered.
-// - fn: The predicate function.
-// = A new list containing the filtered elements.
-List/filter/go
-: ∀(A: *)
-  ∀(cond: Bool)
-  ∀(head: A)
-  ∀(tail: (List A))
-  ∀(fn: ∀(x: A) Bool)
-  (List A)
-= λA λ{
-  #t: λhead λtail λfn
-    #con{head (List/filter A tail fn)}
-  #f: λhead λtail λfn
-    (List/filter A tail fn)
-}
diff --git a/book/List/map.kind b/book/List/map.kind
deleted file mode 100644
index eacfccb69..000000000
--- a/book/List/map.kind
+++ /dev/null
@@ -1,20 +0,0 @@
-// Applies a function to each element of a list.
-// - A: The type of elements in the input list.
-// - B: The type of elements in the output list.
-// - xs: The input list.
-// - fn: The function to apply to each element.
-// = A new list with the function applied to each element of the input list.
-List/map
-: ∀(A: *)
-  ∀(B: *)
-  ∀(xs: (List A))
-  ∀(fn: ∀(x: A) B)
-  (List B)
-= λA λB λ{
-  #nil: λfn
-    #nil{}
-  #con: λxs.head λxs.tail λfn
-    let head = (fn xs.head)
-    let tail = (List/map A B xs.tail fn)
-    #con{ head tail }
-}
diff --git a/book/List/nil.kind b/book/List/nil.kind
deleted file mode 100644
index f26801205..000000000
--- a/book/List/nil.kind
+++ /dev/null
@@ -1,8 +0,0 @@
-// Constructs an empty list.
-// - A: The type of elements in the list.
-// = An empty list of type `(List A)`.
-List/nil
-: ∀(A: *)
-  (List A)
-= λA
-  #nil{}
diff --git a/book/Nat.kind b/book/Nat.kind
deleted file mode 100644
index bb6df00f7..000000000
--- a/book/Nat.kind
+++ /dev/null
@@ -1,9 +0,0 @@
-// Defines the natural numbers (nat) as an inductive datatype.
-// - s: Represents the successor of a nat (x+1).
-// - z: Represents the nat (0).
-Nat
-: *
-= #[]{
-  #z{} : Nat
-  #s{ pred:Nat } : Nat
-}
diff --git a/book/Nat/add.kind b/book/Nat/add.kind
deleted file mode 100644
index 69208411b..000000000
--- a/book/Nat/add.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// Adds two nats.
-// - a: The 1st nat.
-// - b: The 2nd nat.
-// = The sum of `a` and `b`
-Nat/add
-: ∀(a: Nat)
-  ∀(b: Nat)
-  Nat
-= λ{
-  #z: λb b
-  #s: λa.pred λb #s{(Nat/add a.pred b)}
-}
diff --git a/book/Nat/double.kind b/book/Nat/double.kind
deleted file mode 100644
index 05ccaa517..000000000
--- a/book/Nat/double.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// Doubles a nat.
-// - n: The nat to double.
-// = The result of multiplying `n` by 2.
-Nat/double
-: ∀(n: Nat)
-  Nat
-= λ{
-  #z:
-    #z{}
-  #s: λn.pred
-    #s{#s{(Nat/double n.pred)}}
-}
diff --git a/book/Nat/equal.kind b/book/Nat/equal.kind
deleted file mode 100644
index e58d45b52..000000000
--- a/book/Nat/equal.kind
+++ /dev/null
@@ -1,22 +0,0 @@
-// Checks if two nats are equal.
-// - a: The 1st nat.
-// - b: The 2nt nat.
-// = True if `a` and `b` are equal.
-Nat/equal
-: ∀(a: Nat)
-  ∀(b: Nat)
-  Bool
-= λ{
-  #z: λ{
-    #z:
-      #t{}
-    #s: λb.pred
-      #f{}
-  }
-  #s: λa.pred λ{
-    #z:
-      #f{}
-    #s: λb.pred
-      (Nat/equal a.pred b.pred)
-  }
-}
diff --git a/book/Nat/id.kind b/book/Nat/id.kind
deleted file mode 100644
index 3db4256b1..000000000
--- a/book/Nat/id.kind
+++ /dev/null
@@ -1,12 +0,0 @@
-// The identity function for nats.
-// - n: The input nat.
-// = The same nat `n`.
-Nat/id
-: ∀(n: Nat)
-  Nat
-= λ{
-  #z:
-    #z{}
-  #s: λn.pred
-    #s{(Nat/id n.pred)}
-}
diff --git a/book/Nat/match.kind b/book/Nat/match.kind
deleted file mode 100644
index 9448213cc..000000000
--- a/book/Nat/match.kind
+++ /dev/null
@@ -1,16 +0,0 @@
-// Applies a function to a natural number based on its structure.
-// - n: The natural number to match on.
-// - P: A type-level function that determines the return type for each case.
-// - z: The value to return in the zero case.
-// - s: The function to apply in the successor case.
-// = The result of matching on `n`.
-Nat/match
-: ∀(P: ∀(x: Nat) *)
-  ∀(z: (P #z{}))
-  ∀(s: ∀(x: Nat) (P #s{x}))
-  ∀(n: Nat)
-  (P n)
-= λP λz λs λ{
-  #z: z
-  #s: λn.pred (s n.pred)
-}
diff --git a/book/Nat/mul.kind b/book/Nat/mul.kind
deleted file mode 100644
index 4081d61d3..000000000
--- a/book/Nat/mul.kind
+++ /dev/null
@@ -1,14 +0,0 @@
-// Multiplies two nats.
-// - a: The 1st nat.
-// - b: The 2nd nat.
-// = The product of `a` and `b`.
-Nat/mul
-: ∀(a: Nat)
-  ∀(b: Nat)
-  Nat
-= λ{
-  #z: λb
-    #z{}
-  #s: λa.pred λb
-    (Nat/add b (Nat/mul a.pred b))
-}
diff --git a/book/Nat/s.kind b/book/Nat/s.kind
deleted file mode 100644
index a2037ad25..000000000
--- a/book/Nat/s.kind
+++ /dev/null
@@ -1,8 +0,0 @@
-// Constructs the successor of a nat.
-// - n: The nat to which we add 1.
-// = The successor of the nat `n`.
-Nat/s
-: ∀(n: Nat)
-  Nat
-= λn
-  #s{n}
diff --git a/book/Nat/z.kind b/book/Nat/z.kind
deleted file mode 100644
index 1f93d3f4b..000000000
--- a/book/Nat/z.kind
+++ /dev/null
@@ -1,5 +0,0 @@
-// Represents the nat 0.
-// = The nat 0.
-Nat/z
-: Nat
-= #z{}
diff --git a/book/Sigma.kind b/book/Sigma.kind
deleted file mode 100644
index f5c1ce279..000000000
--- a/book/Sigma.kind
+++ /dev/null
@@ -1,13 +0,0 @@
-// Defines a dependent pair type, also known as Sigma type.
-// - A: The type of the first component.
-// - B: A type-level function that determines the type of the second component,
-//      which may depend on the value of the first component.
-// Constructor:
-// - pair: Creates a dependent pair.
-Sigma
-: ∀(A: *)
-  ∀(B: ∀(x: A) *)
-  *
-= λA λB #[]{
-  #new{ fst:A snd:(B fst) }: (Sigma A B)
-}
diff --git a/book/Sigma/fst.kind b/book/Sigma/fst.kind
deleted file mode 100644
index 26aa902b2..000000000
--- a/book/Sigma/fst.kind
+++ /dev/null
@@ -1,8 +0,0 @@
-Sigma/fst
-: ∀(A: *)
-  ∀(B: ∀(x: A) *)
-  ∀(x: (Sigma A B))
-  A
-= λA λB λ{
-  #new: λfst λsnd fst
-}
diff --git a/book/Sigma/snd.kind b/book/Sigma/snd.kind
deleted file mode 100644
index 66e7bb6af..000000000
--- a/book/Sigma/snd.kind
+++ /dev/null
@@ -1,8 +0,0 @@
-Sigma/snd
-: ∀(A: *)
-  ∀(B: ∀(x: A) *)
-  ∀(x: (Sigma A B))
-  (B (Sigma/fst A B x))
-= λA λB λ{
-  #new: λfst λsnd snd
-}
diff --git a/book/String.kind b/book/String.kind
deleted file mode 100644
index 515b6e94a..000000000
--- a/book/String.kind
+++ /dev/null
@@ -1,4 +0,0 @@
-// Defines String as a List of U32 characters.
-// Each U32 represents a Unicode code point.
-String : *
-= (List U32)
diff --git a/book/U32/double.kind b/book/U32/double.kind
deleted file mode 100644
index 7cf8a97e0..000000000
--- a/book/U32/double.kind
+++ /dev/null
@@ -1,4 +0,0 @@
-U32/double
-: ∀(x: U32)
-  U32
-= λx (* x 2)
diff --git a/book/U32/sum.kind b/book/U32/sum.kind
deleted file mode 100644
index 920f419e0..000000000
--- a/book/U32/sum.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-// Calculates the sum of all natural numbers from 0 to x (exclusive).
-// - x: The upper bound of the sum.
-// = The sum of all numbers from 0 to x.
-U32/sum
-: ∀(x: U32)
-  U32
-= λ{
-  0: 0
-  _: λx.pred (+ x.pred (U32/sum x.pred))
-}
diff --git a/book/U32/to_bool.kind b/book/U32/to_bool.kind
deleted file mode 100644
index 93c3c8b4c..000000000
--- a/book/U32/to_bool.kind
+++ /dev/null
@@ -1,10 +0,0 @@
-// Converts a U32 to a Bool.
-// - x: The U32 value to convert.
-// = True if x is non-zero, False otherwise.
-U32/to_bool
-: ∀(x: U32)
-  Bool
-= λ{
-  0: #f{}
-  _: λx.pred #t{}
-}
\ No newline at end of file
diff --git a/book/Vector.kind b/book/Vector.kind
deleted file mode 100644
index 86c4eaa01..000000000
--- a/book/Vector.kind
+++ /dev/null
@@ -1,18 +0,0 @@
-// Defines a vector datatype, which is a list with a known length.
-// - A: The type of elements in the vector.
-// - n: The length of the vector (a Nat).
-// Constructors:
-// - nil: Represents an empty vector.
-// - cons: Adds an element to the front of a vector, increasing its length by 1.
-Vector
-: ∀(A: *)
-  ∀(n: Nat)
-  *
-= λA λn #[]{
-  #nil{} : (Vector A #z{})
-  #cons{
-    len: Nat
-    head: A
-    tail: (Vector A len)
-  } : (Vector A (#s{len}))
-}
diff --git a/book/main.kind b/book/main.kind
deleted file mode 100644
index cb8d3feba..000000000
--- a/book/main.kind
+++ /dev/null
@@ -1,7 +0,0 @@
-main
-: ∀(n: Nat)
-  Nat
-= λ{
-  #s: λpred #z{}
-  #z: #z{}
-}