diff --git a/test.ts b/test.ts
index ba53524..a86845b 100644
--- a/test.ts
+++ b/test.ts
@@ -1,54 +1,76 @@
+import {} from "./typeLevelNats";
+
 type GenericFunction = (...x: never[]) => unknown;
 type Assume<T, U> = T extends U ? T : U;
 
-abstract class TypeFunc {
+abstract class TypeFunc<Arg, Ret> {
   readonly _1?: unknown;
-  new: GenericFunction;
+  new: (_: Arg) => Ret;
 }
 
-type Apply<F extends TypeFunc, _1> = ReturnType<
+type Apply<Arg, Ret, F extends TypeFunc<Arg, Ret>, _1> = ReturnType<
   (F & {
     readonly _1: _1;
   })["new"]
 >;
 
-class Z {
-  private constructor() {}
-  static z(): Z {
-    return new Z();
-  }
+interface GetPrev<N extends Nat> extends TypeFunc<Suc<N>, N> {
+  new: (arg: Suc<N>) => N;
 }
 
-class S<Prev extends Z | S<any>> {
-  public prev: (_: Prev) => Prev;
-  private constructor() {}
-  static s<Prev extends Z | S<any>>(): S<Prev> {
-    return new S();
-  }
+// nat-elim : (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
+// (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
+//
+
+interface ConstNat extends TypeFunc<any, Nat> {
+  new: (_: any) => Nat;
 }
 
-type Nat = Z | S<Nat>;
+interface DoubleSuc extends TypeFunc<Nat, Nat> {
+  new: (arg: Assume<this["_1"], Nat>) => Suc<Suc<typeof arg>>;
+}
 
-interface NatElim<M extends TypeFunc, ZCase extends Apply<M, Z>, SCase extends TypeFunc>
-  extends TypeFunc {
+type NatElim0<
+  M extends TypeFunc<Nat, any>,
+  ZCase,
+  SCase extends TypeFunc<
+    Nat,
+    TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>
+  >,
+  N
+> =
+  /** --------------------------------------------------------------- */
+  N extends Zero // // if N matches Zero
+    ? ZCase //   return ZCase
+    : N extends Suc<infer Prev> // if N matches Suc(Prev)
+    ? Apply<
+        any /* TODO: */,
+        any /* TODO: */,
+        Apply<
+          Nat,
+          TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>,
+          SCase,
+          Prev
+        >,
+        Apply<Nat, any, M, Prev>
+      >
+    : never;
+
+interface DoubleNat extends TypeFunc<Nat, Nat> {
+  new: (arg: Nat) => NatElim0<ConstNat, Zero, DoubleSuc, typeof arg>;
+}
+
+/*
+interface NatElim<
+  MRet,
+  M extends TypeFunc<Nat, MRet>,
+  ZCase extends Apply<infer A, infer R, M<A, R>, Z>,
+  SCase extends TypeFunc
+> extends TypeFunc {
   _unused: (_1: ZCase, _2: SCase) => never;
   new: (arg: Assume<this["_1"], Nat>) => Apply<M, typeof arg>;
 }
 
-interface ConstNat extends TypeFunc {
-  new: (_: unknown) => Nat;
-}
-
-interface DoubleSuc extends TypeFunc {
-  new: (arg: Assume<this["_1"], Nat>) => S<S<typeof arg>>;
-}
-
-interface DoubleNat extends TypeFunc {
-  new: (
-    arg: Assume<this["_1"], Nat>
-  ) => Apply<NatElim<ConstNat, Z, DoubleSuc>, typeof arg>;
-}
-
 type Two = S<S<Z>>;
 
 const realThree: S<S<S<Z>>> = S.s();
@@ -57,6 +79,7 @@ const realFour: S<S<S<S<Z>>>> = S.s();
 function isFour<F extends Apply<DoubleNat, Two>>(_: F) {}
 isFour(realThree);
 isFour(realFour);
+*/
 
 /////
 
diff --git a/typeLevelNats.ts b/typeLevelNats.ts
new file mode 100644
index 0000000..852af15
--- /dev/null
+++ b/typeLevelNats.ts
@@ -0,0 +1,305 @@
+export type Zero = { tag: "Zero" };
+export type Suc<Prev> = { tag: "Suc"; prev: Prev };
+
+const zero: Zero = { tag: "Zero" };
+function suc<Prev>(p: Prev): Suc<Prev> {
+  return { tag: "Suc", prev: p };
+}
+
+type BuildTuple<L extends keyof RealNats, T extends any[] = []> = T extends {
+  length: L;
+}
+  ? T
+  : BuildTuple<L, [...T, "x"]>;
+const _12: BuildTuple<1> = ["x"];
+const _13: BuildTuple<2> = ["x"];
+const _14: BuildTuple<2> = ["x", "x"];
+
+type Tail<L extends any[]> = L extends [unknown, ...infer rest] ? rest : never;
+const _6: Tail<[1, 2, 3]> = [2, 3];
+const _7: Tail<[1, 2, 3]> = [2, 4];
+
+type Length<L extends any[]> = L extends { length: infer len } ? len : never;
+const _8: Length<[3, 4, 5]> = 3;
+const _9: Length<[3, 4, 5]> = 4;
+
+type LengthOfTail<L extends any[]> = Length<Tail<L>>;
+const _10: LengthOfTail<[3, 4, 5]> = 2;
+const _11: LengthOfTail<[3, 4, 5]> = 3;
+
+type Nat<Num extends number> = BuildTuple<Num> extends ["x", ...infer rest]
+  ? Suc<Nat<Length<rest>>>
+  : Zero;
+const _15: ["x"] extends ["x", ...infer _] ? "true" : "false" = "true";
+const _16: ["x"] extends ["x", ...infer _] ? "true" : "false" = "false";
+
+const _17: [] extends ["x", ...infer _] ? "true" : "false" = "true";
+const _18: [] extends ["x", ...infer _] ? "true" : "false" = "false";
+
+const _1: Nat<0> = zero;
+
+const _3: Nat<1> = suc(zero); // should pass
+const _2: Nat<1> = zero; // should fail
+
+const _5: Nat<4> = suc(suc(suc(suc(zero)))); // should pass
+const _4: Nat<4> = suc(suc(suc(zero))); // should fail
+
+type RealNats = [
+  0,
+  1,
+  2,
+  3,
+  4,
+  5,
+  6,
+  7,
+  8,
+  9,
+  10,
+  11,
+  12,
+  13,
+  14,
+  15,
+  16,
+  17,
+  18,
+  19,
+  20,
+  21,
+  22,
+  23,
+  24,
+  25,
+  26,
+  27,
+  28,
+  29,
+  30,
+  31,
+  32,
+  33,
+  34,
+  35,
+  36,
+  37,
+  38,
+  39,
+  40,
+  41,
+  42,
+  43,
+  44,
+  45,
+  46,
+  47,
+  48,
+  49,
+  50,
+  51,
+  52,
+  53,
+  54,
+  55,
+  56,
+  57,
+  58,
+  59,
+  60,
+  61,
+  62,
+  63,
+  64,
+  65,
+  66,
+  67,
+  68,
+  69,
+  70,
+  71,
+  72,
+  73,
+  74,
+  75,
+  76,
+  77,
+  78,
+  79,
+  80,
+  81,
+  82,
+  83,
+  84,
+  85,
+  86,
+  87,
+  88,
+  89,
+  90,
+  91,
+  92,
+  93,
+  94,
+  95,
+  96,
+  97,
+  98,
+  99,
+  100,
+  101,
+  102,
+  103,
+  104,
+  105,
+  106,
+  107,
+  108,
+  109,
+  110,
+  111,
+  112,
+  113,
+  114,
+  115,
+  116,
+  117,
+  118,
+  119,
+  120,
+  121,
+  122,
+  123,
+  124,
+  125,
+  126,
+  127,
+  128,
+  129,
+  130,
+  131,
+  132,
+  133,
+  134,
+  135,
+  136,
+  137,
+  138,
+  139,
+  140,
+  141,
+  142,
+  143,
+  144,
+  145,
+  146,
+  147,
+  148,
+  149,
+  150,
+  151,
+  152,
+  153,
+  154,
+  155,
+  156,
+  157,
+  158,
+  159,
+  160,
+  161,
+  162,
+  163,
+  164,
+  165,
+  166,
+  167,
+  168,
+  169,
+  170,
+  171,
+  172,
+  173,
+  174,
+  175,
+  176,
+  177,
+  178,
+  179,
+  180,
+  181,
+  182,
+  183,
+  184,
+  185,
+  186,
+  187,
+  188,
+  189,
+  190,
+  191,
+  192,
+  193,
+  194,
+  195,
+  196,
+  197,
+  198,
+  199,
+  200,
+  201,
+  202,
+  203,
+  204,
+  205,
+  206,
+  207,
+  208,
+  209,
+  210,
+  211,
+  212,
+  213,
+  214,
+  215,
+  216,
+  217,
+  218,
+  219,
+  220,
+  221,
+  222,
+  223,
+  224,
+  225,
+  226,
+  227,
+  228,
+  229,
+  230,
+  231,
+  232,
+  233,
+  234,
+  235,
+  236,
+  237,
+  238,
+  239,
+  240,
+  241,
+  242,
+  243,
+  244,
+  245,
+  246,
+  247,
+  248,
+  249,
+  250,
+  251,
+  252,
+  253,
+  254,
+  255,
+  256
+];