This video tries to be a brief introduction to Type Theory. I am sorry for the inaccuracies or potential errors. Feel free to tell me in the comments, I just started learning about this topic but I found it too amazing not to share.

As you probably already can tell, this is my first video speaking in English so I do hope everything can be understood clearly. My pronunciation is not the nicest.

Also this is my entry to SoME1.

Music credits:
 - "Inspiration Piano - Calm Background Music For Videos" by Lesfm.
 - "Dreamland" by Aakash Gandhi.
 - "Sea of Memory" by Aakash Gandhi.

To prove a theorem, we use other theorems.

And in order to prove them as well, we use other ones.

And so on, making up a gigantic pyramid of theorems, until we reach the first theorems.

These first theorems are proven using actions.

Actions are propositions we assume to be true without requiring a proof, so we want them to be as simple as possible.

Such as the shortest distance between 2 points is a straight line.

Even though we often want actions to feel intuitive, they are completely arbitrary.

If we change the actions, the theorems will be different.

The only thing we must avoid is to have a set of actions that would allow 2 contradictory theorems to be true at the same time.

Sadly, Kurt Gödel has proven that there is no way to know if our theory is consistent or not.

Instead, we can only hope it to be consistent as long as we don't find any contradiction.

The most commonly used set of actions is called ZF, which is a set theory.

In a set theory, all mathematical objects are sets.

But also, the actions of set theory are built onto logic.

Logic is a set theory that tells us how to manipulate propositions.

These propositions can be combined using logic rules to create new propositions.

But today, I want to talk about an alternative to set theory, type theory.

Type theory is better suited for proof assistants.

Proof assistants are programs that can tell whether your proof is correct or incorrect.

If you are a programmer, you probably already encountered types like the boolean type, the string type, or the integer type.

If you are not, you just have to know that we group objects of the same kind under a type.

In order to better understand types, let's construct some basic ones.

If you don't know what a boolean is, it's just a value that can either be true or false.

So in order to build the type, we need to define how to construct elements of that type.

In that case, since there are only 2 elements, we can be exhaustive and say we can either construct true or false.

We will define nat, the type of all natural numbers.

We might be tempted to have a constructor for every number, but the problem with that approach is not only the definition is infinite, but we also don't have a nice structure for the type.

So instead we will just have 2 constructors, 0 of type Nat, and a function that can take a number and return another 1.

Then we can define the numbers 1, 2, 3 and so on by iterating over the function.

We can also combine types to create new types.

For instance, if you have the types A and B, you can create the function type that takes an object of type A and returns an object of type B.

You can also create the pair type A times B, whose elements are pairs composed of an element of A and an element of B.

With that, let's try to define the sum function.

This function will take 2 natural numbers and return their sum.

First, let's remember there are only 2 options for a nut.

It can only be 0 or the successor of another nut.

We will split the definition of sum in 2 cases, if the first input is 0, or if the first input is the successor of another number.

If it's 0, then we're just trying to sum 0 and b, so we will just return b.

If it's not, we can sum the predecessor of A and B and take the successor of the whole.

Using these definitions, we can perform additions.

Take a moment to convince yourself and appreciate the fact that this will always work.

Remember when I said set theory is built onto logic?

Well, that's not the case for type theory.

Type theory handles logical propositions by itself using a very outstanding correspondence.

Types can be seen as logical propositions.

And an inhabitant of this type can be seen as a proof of a proposition.

If the type has several inhabitants, that means there are several proofs of the proposition.

And if it has none, that means the proposition is unprovable.

Doesn't mean it's true or false, just that you can't prove it.

For instance, the function type from A to B can be understood as an implication, Because if this type has an inhabitant, that means you have a function that can take any element of type A and convert it to an element of type B.

And an element of type A can be seen as a proof of A on an element of type B as a proof of B.

So your function is converting any proof of A to a proof of B.

So since you can derive B from A with this function, that means A implies B.

A times B also can be interpreted as a logical proposition.

It's the logical N, because in order to have an element of type A times B, you need both an element of A and an element of B.

So, in terms of logic, that means, in order to prove A and B, you need a proof of A and a proof of B.

There also are other types I haven't introduced that correspond to other logical propositions.

This can be a bit tricky to wrap your head around this concept at first, but this is truly beautiful to me.

If there is anything you have to prove, just take its corresponding type and try to find an element of it.

There is a last very important type I wanna show you.

In type theory, we have a function called identity.

This function takes 2 nuts, a and b, and returns the type A equals B.

It may seem a bit weird at first because this function returns a type.

So now we have a type for every possible equality proposition But does that mean everything is equal to every other thing in type theory?

No, of course not Because we have to remember the proposition is true only if we can find an inhabitants of the corresponding type So let's see how to construct inhabitants of the equality type.

There is a single constructor called waffle.

Waffle takes a single number and returns an element of the type this number is equal to itself.

So like Waffle of 2 is an element of the type 2 equals 2.

You can see Waffle as an action that states that every number is equal to itself.

Hence its name that stands for Wafflexivity.

With all that knowledge, let's try to prove in type theory that 2 plus 2 equals 4.

First we have to take the corresponding type of a proposition, and now we will try to construct an element of the type.

We will first apply Waffle to 2 plus 2, which will give us an element of the type 2 plus 2 equals 2 plus 2.

But since 2 plus 2 with this is 2, 4, the type 2 plus 2 equals 2 plus 2 is the same as the type 2 plus 2 equals 4.

So, refer of 2 plus 2 is actually a proof that 2 plus 2 equals 4.

As I said in the beginning of this video, most proof assistants use type theory.

1 proof assistant that I really like is Lin.

So as a conclusion I want to show You you


Speaker 0: To prove a theorem, we use other theorems. And in order to prove them as well, we use other ones. And so on, making up a gigantic pyramid of theorems, until we reach the first theorems. These first theorems are proven using actions. Actions are propositions we assume to be true without requiring a proof, so we want them to be as simple as possible.

Such as the shortest distance between 2 points is a straight line. Even though we often want actions to feel intuitive, they are completely arbitrary. If we change the actions, the theorems will be different. The only thing we must avoid is to have a set of actions that would allow 2 contradictory theorems to be true at the same time. If that happens, everything falls apart.

Sadly, Kurt Gödel has proven that there is no way to know if our theory is consistent or not. Instead, we can only hope it to be consistent as long as we don't find any contradiction. The most commonly used set of actions is called ZF, which is a set theory. In a set theory, all mathematical objects are sets. But also, the actions of set theory are built onto logic.

Logic is a set theory that tells us how to manipulate propositions. These propositions can be combined using logic rules to create new propositions. But today, I want to talk about an alternative to set theory, type theory. Type theory is better suited for proof assistants. Proof assistants are programs that can tell whether your proof is correct or incorrect.

Isn't that cool? In type theory, every object has a type. If you are a programmer, you probably already encountered types like the boolean type, the string type, or the integer type. Well, that's the same in type theory. If you are not, you just have to know that we group objects of the same kind under a type.

In order to better understand types, let's construct some basic ones. We will start with a boolean type. If you don't know what a boolean is, it's just a value that can either be true or false. And that's it. So in order to build the type, we need to define how to construct elements of that type.

In that case, since there are only 2 elements, we can be exhaustive and say we can either construct true or false. And with that, we have our first type. So that was easy. Let's build a more complex 1. We will define nat, the type of all natural numbers.

We might be tempted to have a constructor for every number, but the problem with that approach is not only the definition is infinite, but we also don't have a nice structure for the type. So instead we will just have 2 constructors, 0 of type Nat, and a function that can take a number and return another 1. Then we can define the numbers 1, 2, 3 and so on by iterating over the function. We can also combine types to create new types. For instance, if you have the types A and B, you can create the function type that takes an object of type A and returns an object of type B.

You can also create the pair type A times B, whose elements are pairs composed of an element of A and an element of B. With that, let's try to define the sum function. This function will take 2 natural numbers and return their sum. First, let's remember there are only 2 options for a nut. It can only be 0 or the successor of another nut.

We will split the definition of sum in 2 cases, if the first input is 0, or if the first input is the successor of another number. If it's 0, then we're just trying to sum 0 and b, so we will just return b. If it's not, we can sum the predecessor of A and B and take the successor of the whole. Using these definitions, we can perform additions. Take a moment to convince yourself and appreciate the fact that this will always work.

Remember when I said set theory is built onto logic? Well, that's not the case for type theory. Type theory handles logical propositions by itself using a very outstanding correspondence. Types can be seen as logical propositions. And an inhabitant of this type can be seen as a proof of a proposition.

If the type has several inhabitants, that means there are several proofs of the proposition. And if it has none, that means the proposition is unprovable. Doesn't mean it's true or false, just that you can't prove it. For instance, the function type from A to B can be understood as an implication, Because if this type has an inhabitant, that means you have a function that can take any element of type A and convert it to an element of type B. And an element of type A can be seen as a proof of A on an element of type B as a proof of B.

So your function is converting any proof of A to a proof of B. So since you can derive B from A with this function, that means A implies B. A times B also can be interpreted as a logical proposition. Can you see which 1? It's the logical N, because in order to have an element of type A times B, you need both an element of A and an element of B.

So, in terms of logic, that means, in order to prove A and B, you need a proof of A and a proof of B. There also are other types I haven't introduced that correspond to other logical propositions. This can be a bit tricky to wrap your head around this concept at first, but this is truly beautiful to me. So what is the proof in type theory? If there is anything you have to prove, just take its corresponding type and try to find an element of it.

There is a last very important type I wanna show you. It's the equality type. In type theory, we have a function called identity. This function takes 2 nuts, a and b, and returns the type A equals B. It may seem a bit weird at first because this function returns a type.

So now we have a type for every possible equality proposition But does that mean everything is equal to every other thing in type theory? No, of course not Because we have to remember the proposition is true only if we can find an inhabitants of the corresponding type So let's see how to construct inhabitants of the equality type. There is a single constructor called waffle. Waffle takes a single number and returns an element of the type this number is equal to itself. So like Waffle of 2 is an element of the type 2 equals 2.

You can see Waffle as an action that states that every number is equal to itself. Hence its name that stands for Wafflexivity. With all that knowledge, let's try to prove in type theory that 2 plus 2 equals 4. First we have to take the corresponding type of a proposition, and now we will try to construct an element of the type. We will first apply Waffle to 2 plus 2, which will give us an element of the type 2 plus 2 equals 2 plus 2.

But since 2 plus 2 with this is 2, 4, the type 2 plus 2 equals 2 plus 2 is the same as the type 2 plus 2 equals 4. So, refer of 2 plus 2 is actually a proof that 2 plus 2 equals 4. As I said in the beginning of this video, most proof assistants use type theory. 1 proof assistant that I really like is Lin. So as a conclusion I want to show You you

See all Dapper Mink transcripts on Youtube

Why should you learn Type Theory?