diff --git a/README.md b/README.md
new file mode 100644
index 0000000..c5c234a
--- /dev/null
+++ b/README.md
@@ -0,0 +1,385 @@
+---
+author: Nathan McCarty
+title: "Idris 2: Natural Numbers"
+---
+
+# Script
+
+This video is going to be a trial run of a format that I want to use for
+a longer running series teaching the [Idris
+2](id:584e89dc-61f7-4c57-a6a4-72c5470c3280) programming language and the
+basics of programming with dependent types.
+
+We'll kick things off by examining a core concept that crops up
+everywhere in programming, and breaking down how the formalism of it
+works.
+
+## What is a "number"
+
+This may seem like a bit of a crazy question, everyone knows what
+numbers are, numbers are these values that we can do addition,
+subtraction, etc, on and get more numbers back out, right?
+
+However, to be able to make mathematical guarantees about our programs,
+we need to break the concept of number down to its basic parts and
+formalize what we mean by "addition" and "multiplication"
+
+To make things a bit simpler, for now we'll restrict our discussion of
+numbers to the natural numbers: zero and the positive whole numbers.
+We'll be using a common formalism known as Peano Arithmetic
+
+## Peano Axioms
+
+We'll go through the relevant peano axioms, one by one, implementing
+them as we go. Don't be scared by the term "axiom", it's just
+mathematical jargon for "basic assumption".
+
+The historical peano axioms are:
+
+1. Zero is a natural number
+2. For all x, x = x equality is reflexive
+3. For all x and y, if x = y, then y = x equality is symmetric
+4. For all x, y, and z, if x = y and y = z, then x = z equality is
+ transitive
+5. for all a and b, if a is a natural number, and a = b, then b is a
+ natural number The naturals are closed under equality
+6. For every natural number, S(n) is a natural number The naturals are
+ closed under S
+7. For all natural numbers m and in, if S(m) = S(n), then m = n S is an
+ injection
+8. For every natural number, S(n) = 0 is false
+
+Idris provides, in a way, a more powerful logic than the one peano
+arithmetic was originally conceived in, so we will be proving some of
+these statements rather than assuming them as axioms, and many of theses
+proofs will turn out to be "freebes".
+
+We'll start out by defining a `Natural` data type.
+
+### Building the data type
+
+1. Zero is a natural number
+
+ We can assert that zero is a natural number by simply creating a
+ constructor representing zero, giving us axiom 1.
+
+2. For every natural n, S(n) is a natural number
+
+ `S(n)` is the successor function, it's equivalent to taking a
+ natural number and adding one to it. We'll implement this by taking
+ a constructor `S` which takes a natural number as an argument, and
+ returns the natural number `S(n)`
+
+ Now that we have these two constructors, we can start to define
+ representations of some common numbers that we might want to use
+
+ The type signature of the constructor provides us with axiom 6
+
+3. For every natural number n, n = n
+
+ The first thing we want to be able to say about natural numbers is
+ that every natural is equal to itself.
+
+ To say this, we'll need a notion of equality, we can do this by
+ defining another type that starts to invoke some dependent magic,
+ we'll call it `Equality`. This type will take two natural numbers as
+ value arguments, so we can say, for example, the type of a value is
+ `Equality n m` where n and m are natural numbers.
+
+ The equality type provides one constructor, `Reflexive`,
+ traditionally this is shortened to `Refl`, but we'll keep it long
+ hand for teaching purposes. This constructor states that equality
+ over the naturals is reflexive, meaning that every natural number is
+ equal to itself, giving us axiom 2.
+
+ This constructor enforces equality by only taking one natural as an
+ implicit argument, and then using it for both "slots" in the type.
+ So long as this is the only constructor of the type, if we are
+ holding a value of type `Equality m n`, then we know that `m` and
+ `n` must be the same number, as that's the only way to construct
+ such a value.
+
+ The definition of the constructor for the equality type,
+ `Reflexive`, provides us with axiom 2, and the "kind", or
+ type-of-the-type, provides us with axiom 5
+
+### Writing some proofs
+
+Now we'll transition into writing some proofs, this requires a bit of a
+detour into what a proof is.
+
+1. Proving positives
+
+ The logic we use in Idris is what is known as constructive, to prove
+ a statement, you must construct an example of it. For example, to
+ prove that the number "two" exists, we construct the value "two" and
+ return it, and to prove that two numbers m and n are equal, we
+ construct an instance of type `Equality m n` and return it
+
+2. A detour into totality
+
+ There is one caveat with using functions returning values as proofs,
+ in order for the resulting logic to be sound, all the functions
+ involved must be "total".
+
+ We say that a function is "total" when it returns a value in finite
+ time, without crashing, for all possible inputs. A non-total
+ function can be used to prove nonsense statements by either never
+ returning or by being undefined for a particular input.
+
+ Idris helpfully includes a totality checker, we'll go ahead and use
+ a compiler directive to ask idris to signal an error if any of our
+ functions are non-total.
+
+ Some of you may be screaming at your screen about the halting
+ problem right now, and don't worry, we'll get into detail about how
+ the totality checker works later, but for now we'll just say that
+ it's not a complete solution, it doesn't work automatically for
+ every program, and both can and will result in false negatives for
+ programs that aren't structured in such a way that proving totality
+ is more or less trivial, requiring either manual proving or
+ restructuring the program.
+
+ Now that we have `%default total`, we can go ahead and prove an
+ example equality
+
+3. Proving a negative
+
+ In constructive logic, the way you establish a negative, a "not X"
+ statement, is to show that the statement results in a contradiction.
+
+ In idris, this looks like a function which is total and returns a
+ value of an empty type. Since the return type has no possible
+ values, and the function is total, and thus must return in finite
+ time for all possible inputs, the impossibility of returning
+ speaks to the impossibility of at least one of the inputs.
+
+ We'll demonstrate this by proving that zero is not equal to one, by
+ writing out a function that takes an `Equality 0 1` as it's input
+ and returns void. As a value of the type `Equality 0 1` is
+ structurally impossible, idris lets us use the `impossible` keyword
+ to signify that this function is impossible to call in a well-typed
+ program.
+
+4. For all x and y, if x = y then y = z (symmetric)
+
+ This property, formally stating that equality over the naturals is
+ symmetric, takes the form of a function with two naturals, x and y,
+ as arguments, as well as an `Equality x y`, turning that into an
+ `Equality y x`. Totality here provides us an assurance that this
+ works for all possible inputs
+
+ This turns out to be nearly trivial to prove in Idris's logic, by
+ simply writing out the function, and pattern matching the
+ `Equality x y` argument to it's `Reflexive` constructor, idris
+ realizes that the two naturals must be the same value and "rewrites"
+ y into x, changing our output type to `Equality x x`, which we can
+ return simply with the `Reflexive` constructor, making use of the
+ 'indiscernability of identicals' principle, and giving us axiom 3.
+
+5. For all x, y, and z, if x = y and y = z, then x = z
+
+ We'll state this one as a function taking naturals x, y, and z, an
+ `Equality x y`, and a an `Equality y x`, and returning an
+ `Equality x z`
+
+ Much like the previous example, Idris also gives us this one "for
+ free", we can simply pattern match both `Equality` arguments down to
+ their `Reflexive` constructors, "rewriting" the output type into
+ `Equality x x`, which can again be created simply with the
+ `Reflexive` constructor, giving us axiom 4
+
+6. For all x and y, if S(x) = S(y), then x = y
+
+ We'll state this one as function taking naturals x and y, and an
+ `Equality S(x) S(y)`, returning an `Equality x y`.
+
+ Much like the previous two, this is another freebe from idris,
+ pattern matching on the equality argument "rewrites" the output type
+ to `Equality x x`, giving us axiom 7 with another simple invocation
+ of the `Reflexive` constructor
+
+7. For every n, S(n) != 0
+
+ This one is a little more interesting, we'll phrase it as a function
+ taking a natural n, an `Equality (S n) Zero`, and returning Void.
+
+ This still ends up being a bit of a freebe, however, since a value
+ of the type `Equality (S n) Zero` is structurally impossible, idris
+ lets us use the impossible keyword, giving us axiom 8
+
+## Implementing Operations
+
+Now that we have our natural numbers defined, and have proven that they
+obey the peano axioms, we can start to implement some operations over
+them. For the sake of keeping this video reasonable in length, we'll
+only be implementing addition, but the other familiar operations, like
+subtraction, multiplication, and division can also be implemented over
+peano numbers.
+
+### Defining Addition
+
+Addition over the natural numbers is a function of two arguments with
+the following properties:
+
+- Zero is the identity (x + 0 = x) Both left and right
+- Commutative (x + y = y + x)
+- Associative (x + (y + z) = (x + y) + z)
+
+We'll go ahead and write these out as types before we implement
+anything, then we'll go ahead and implement the definition of addition
+over the peano numerals.
+
+This is a pretty simple recursive definition, if the right argument is
+zero, return the left argument, but if the right argument is a
+successor, return the successor of the right argument plus the number
+the right argument is the successor of.
+
+This can be seen as a structural replacement of the `Zero` at the bottom
+of the right argument's "stack" with the value of the left argument
+(draw example)
+
+### Proving identity
+
+The proof that zero is the identity is trival for the case when the zero
+is on the right, as we are just "replacing" the zero with the other
+value.
+
+The case where the Zero is on the left is a little bit more complex.
+Pattern matching the argument, the branch where the argument is Zero is
+trivial. In the other branch, we recurse on the value our argument is a
+successor of.
+
+We now need a way to turn `Equality x y` into `Equality (S x) (S y)`, so
+we define a new `eqSucc` utility, and have the compiler implement it for
+us.
+
+Now that we have our eqSucc utility, we can call it on the equality we
+generated via recursion and call our function complete.
+
+This isn't the only way we could have implemented this function, we
+could have applied the symmetry axiom as a "rewriting rule" to transform
+the statement being proved into the left-handed version, and while the
+standard library provides the mechanics for this, they are based on the
+built in equality type, not our bespoke one, and those mechanics are out
+of scope for this video
+
+### Proving the commutative property
+
+We'll start off by pattern matching our right argument, to match the
+structure of `plus`. The zero case is pretty simple, It's actually just
+our `zeroIdentityLeft` statement
+
+Pattern matching the left argument, we can see that our new zero case is
+just our `zeroIdentityLeft` with a successor slapped on each side, so we
+pull out `eqSucc` and get that branch done
+
+We then recursively call commutative to get a lemma, using the inner,
+decreased, value of m, but the full value of n. This still gives us
+totality because the m argument is decreasing towards the base case, but
+gives us back something that's almost our output type, minus an
+applicaton of `eqSucc`. We notice that the resulting equality has an `S`
+in the wrong place on the right hand side, so we'll sketch out a helper
+function to do that rearrangement for us.
+
+This helper function is a true statement, rest assured, but it is rather
+annoying to prove without rewriting rules, so we'll leave this one
+unimplemented for now, and touch on it again in a later episode
+
+We have now proven, assuming that for all n and m `(S (plus m n))` is
+equivalent to `(plus (S m) n)`, addition commutes.
+
+### Proving the associative property
+
+The associative property is somewhat easy to prove with access to
+rewriting rules, but complicated without them, so we'll again leave this
+for a future video where we investigate the standard library types.
+
+## Correspondence with the integers
+
+The peano arithmetic implementation of natural numbers has some pros, it
+has almost no moving parts, it's easy to reason about, and naturally
+lends itself to recursive inductive proofs, but it also has some major
+downsides. As peano numerals are basically just linked lists where the
+length of the list is the number we are encoding, they are horribly
+space inefficient and operations are much slower than they really need
+to be.
+
+It would be great if we could keep the ease of reasoning, but still
+represent peano numeral as space and time efficient machine integers.
+
+### Idris already does part of this for us
+
+It turns out that, as reasoning about numbers is such a fundamental part
+of theorem proving and working with dependent types, idris has an
+optimization that does this shifting of representation for us.
+
+Any time idris sees a data structure that looks enough like the peano
+definition of natural numbers, it will automatically optimize it's
+runtime representation to an `Integer`, and we can enforce this with the
+`%builtin Natural` pragma
+
+### Creating conversion functions
+
+Idris's natural optimization very helpfully also applies to functions
+that convert between naturals and integers, but we must be careful in
+how we write them.
+
+We'll start by writing out the type signature for the `natToInteger`
+function from Naturals to Integers and explain the conditions as we go:
+
+1. Exactly one argument must be pattern matched on This applies in our
+ case because there is exactly one argument
+2. The right hand side of the `Zero` case must be 0
+3. The right hand side of the successor case must be
+ `1 + natToInteger k`
+
+With all these criteria met, idris will helpfully optimize our
+`natToInteger` function to a constant time operation
+
+Going the other direction is a little bit more complicated, for
+`integerToNat` we will be using the `%builtin IntegerToNatural` pragma,
+which will give us an error if the optimization does not apply.
+
+The first thing we need to do is check if the integer is negative, and
+short circuit to 0 if it is. In the case that the integer is positive,
+we branch on its value, returning `Zero` for the zero case, and
+recursing in the non-zero case
+
+This complains about totality, so we'll assert that `i - 1` is
+structurally smaller than `i`, which is valid here as `i` will strictly
+decrease down to 0, which is our base case. We'll go into more detail in
+a future episode about how to properly make the compiler happy
+here.
+
+We now apply our builtin pragma to make sure the function works as
+expected, and we now have our constant-time casting operations
+implemented.
+
+### Replacing our operations at runtime with operations over integers
+
+Idris provides us with a helpful pragma, `%transform`, which tells idris
+that we want it to rewrite an expression into another in the runtime
+environment.
+
+We can use this on our natural number operations to make them constant
+time as well, such as plus The idris standard library makes heavy use of
+`%transform` for it's natural number operations, making natural numbers
+much more efficient to work with than you might expect
+
+## Conclusion
+
+This video was, first and foremost, intended to be a test of the format,
+and give me a chance to get my recording and editing workflow setup
+before diving into it more seriously, so I've left a lot unsaid and this
+probably feels terribly unmotivated.
+
+While I hope I've managed to provide a taste of what theorem proving and
+dependent typing has to offer in this little adventure through
+re-implementing natural numbers from first principals, the next video in
+this series, the first proper entry, will consist of a lot more down to
+earth programming. We'll start off without anything in the way of proofs
+or dependent types, and get a feel for what idris is like to
+program in, building back up from there, giving proper context,
+more insight, and more detailed explanations to the concepts we covered
+here as we go along.
diff --git a/src/Naturals.idr b/src/Naturals.idr
index 5b86564..b5f5b65 100644
--- a/src/Naturals.idr
+++ b/src/Naturals.idr
@@ -8,6 +8,22 @@ data Natural : Type where
||| The successor of a natural n is a natural
S : Natural -> Natural
+%builtin Natural Natural
+
+natToInteger : Natural -> Integer
+natToInteger Zero = 0
+natToInteger (S x) = 1 + (natToInteger x)
+
+integerToNat : Integer -> Natural
+integerToNat i =
+ if i < 0
+ then Zero
+ else case i of
+ 0 => Zero
+ _ => S (integerToNat (assert_smaller i (i - 1)))
+
+%builtin IntegerToNatural Naturals.integerToNat
+
one : Natural
one = S Zero
@@ -40,6 +56,8 @@ plus : (n, m : Natural) -> Natural
plus n Zero = n
plus n (S x) = S (n `plus` x)
+%transform "plus" Naturals.plus n m = Naturals.integerToNat (Naturals.natToInteger n + Naturals.natToInteger m)
+
zeroIdentityRight : (n : Natural) -> Equality n (n `plus` Zero)
zeroIdentityRight n = Reflexive