---
title: 'Introducing Type Theory: Spilling the Tea'
source: 'https://youtube.com/watch?v=5xBVdS4DO3U'
video_id: '5xBVdS4DO3U'
date: 2026-07-31
duration_sec: 1094
---

# Introducing Type Theory: Spilling the Tea

> Source: [Introducing Type Theory: Spilling the Tea](https://youtube.com/watch?v=5xBVdS4DO3U)

## Summary

This video is the first part of a series introducing Martin-Löf type theory. It covers the motivation for typed systems, basic types (unit and empty), function types, and the Curry-Howard correspondence, demonstrating how logical proofs can be constructed as typed programs.

### Key Points

- **Problems with Untyped Calculus** [00:17] — Untyped lambda calculus can crash with infinite recursion and allow nonsensical operations like putting numbers into boolean functions; type theory solves these issues.
- **Series Roadmap** [00:31] — Part 1 covers the empty type, unit type, and function type, plus the Curry-Howard correspondence; later parts cover product/sigma/equality types and type families.
- **Primary Resource** [01:25] — The series is based on Martin-Löf type theory as used in Homotopy Type Theory: Univalent Foundations of Mathematics.
- **Types and Inhabitance** [01:54] — Every entity has exactly one type, written 'object : Type'; an entity inhabits a type if it is of that type.
- **Unit Type** [02:36] — The unit type, written as bold 1, is inhabited by the single object Point.
- **Empty Type** [02:52] — The empty type is defined as uninhabited — no entity has this type.
- **Function Types** [03:23] — A function type is written as domain → codomain, representing the type of the argument and return value.
- **Totality** [03:40] — In type theory, functions must be total: for every element of the domain, the function must produce an element of the codomain.
- **Unit → Empty is Uninhabited** [04:31] — No function can map Point to an element of empty, because empty has no elements; the 'trade offer' cannot be fulfilled.
- **Empty → Unit is Inhabited** [05:16] — With no inputs to satisfy, the function is trivially total; you can promise anything when nobody can call you on it.
- **Curry-Howard Correspondence** [13:57] — Propositions correspond to types, proofs correspond to programs inhabiting those types, and implication corresponds to function types.
- **Typed Hole Method** [14:29] — Start with a hole of the goal type; introduce abstractions for each function type and use available variables/functions to fill the remaining holes.

### Conclusion

Type theory provides a unifying framework where mathematical proofs become programs, eliminating the ambiguity of natural language and the bugs of untyped lambda calculus.

## Transcript

calculus with two showstoppers first it was possible to make it crash and explode into infinite recursion also you could do silly things like put numbers into Burling functions and strings into numerical functions with all sorts of
chaos resulting in this video we are going to solve both of those problems by using type Theory but type theory is such a large topic so we are going to such a large topic so we are going to cover it in three parts in this video
I'm going to introduce the empty type the unit type and function type then I'm going to tell you all about the C Howard correspondence a powerful result that allows us to link computer programming with the writing of mathematical proof
in the next video I'm going to introduce product types some types and equality type finally in the last video of this subsequence we will cover type families
P types Sigma types and the natural numbers these videos are going to introduce you to a form of Martin LOF type Theory there are other type theories out there but once you have a
handle on one of them under your belt you'll be able to convert your knowledge to the other type also it is the type used in homotopy type Theory univ
univariant foundations of mathematics which is my primary resour resource for this video when I say it's my primary resource I mean that if I say anything correct about type Theory it is most likely from this book and if there are
likely from this book and if there are any mistakes it is most likely from me misunderstanding it in type Theory everything has a property called its type and entity's type basically tells you what it is and we write the type
you what it is and we write the type like this the object then a colon then the object's type and entity can only have one type so the counting number one is a distinct object from the rational number one this might sound strange to
you initially but the two ones have different properties you can divide the rational one by two but you can't do that to the counting number one you can subtract two from the rational number one again something you can't do with
counting number one we say an entity inhabits a type if that thing is of that type and we say a type is inhabited if an object of that type exists example
time let's introduce a few simple type the unit type this is written by a bold number one and is defined to be inhabited by the single object Point by definition this is the only object which is within this type another useful type
is the empty type it is defined as being uninhabited in other words there is no entity with this type Now by themselves they're not that interesting and didn't we introduce typing to fix problems with Lambda Expressions well let's create a
Lambda Expressions well let's create a type for functions in type Theory functions also have types A functions type is expressed like this domain to co- domain so the type of the thing the function takes as an argument a little
arrow and then the thing that the function will return on application like all types a fun function type can be inhabited or uninhabited and we can show a function type is inhabited by writing an example function which complies with
that function's type one of the most fundamental rules of type theory is that these functions must be total that is for every element inhabiting the domain
for every element inhabiting the domain the function has to be able to produce some element that inhabits the co- domain let's look at the function type unit to unit as an example it is simple to show that this function is inhabited
giving the example function of X of type Unit maps to X of type unit we could also write this as point of type Unit maps to point of type unit when we have
multiple entities inhabiting a type we can use this style of using an entity rather than a variable on the left hand side to say which values map to which
how about the function type unit to empty well the requirement is that for every item in the domain we have to be able to produce an element from the codomain however there is nothing in empty if a function is called with Point
as an argument it can't return an element from empty because there's simply none of them in a way a function type is like a trade offer it says if type is like a trade offer it says if you give me a thing of domain type then
I will give you an object of co- domain type with the co- domain type being empty it is impossible to fulfill this deal because there's simply nothing to deal because there's simply nothing to give how about empty to unit well the
condition we have to fulfill is there has to be an output for every possible input but if there are no input elements it is Trivial to fulfill this condition
now this might sound weird but think about the trade offer analogy but think about the trade offer analogy you can offer anything so long as you know that nobody will ever take you up on that offer the same reasoning works
for empty to empty this is also inhabited because there's no way we can call the bluff on the function in this situation we can generalize this and
make a handy chart of how inhabited and uninhabited types relate to function types let's stick this chart up in the corner of the screen I am sure it will not become important or relevant at all in this video's
then you most likely watched other maths videos where somebody gives a convincing argument about why some mathematical fact is true most likely along with a well animated diagram you might even think to yourself why do we have all
these symbols and proofs in mathematics can't we just do it with diagrams and explanation and honestly you're not wrong for the vast majority of mathematics histories diagrams and explanations is how maths worked however
as math developed it got more and more abstract and further and further away abstract and further and further away from our concrete day-to-day experiences some of this was due to things like differential and integral calculus
making us have to deal with Infinities physics starting to deal with scales so much larger and smaller than we normally expected it just turns out that yeah that seems right starts to stop working in the spaces where we don't have much
day-to-day experience the solution to this is when we had a math fact that we were not quite sure of we would start with the math facts that that everybody agrees with that were true then take small steps and reasonings steps that
were so small and so simple that it was easy to check them for errors until we took enough steps to get to the fact that we wish to check a maath fact that
might be right or might be wrong is called a proposition the things that called a proposition the things that everybody agrees on are true are called axioms and the collection of small steps that we are allowed to take from Axion
towards propositions is called our Logic the string of logical Steps From what is the string of logical Steps From what is known to what is we wish to prove is called a proof rather than using English French Japanese or some other natural
language that can be ambiguous mathematicians started to create a mathematicians started to create a compact unambiguous system of symbols this is very powerful but it does mean to access the heart of mathematics you
have to learn a new language which does create a problem for people doing math education because you have to teach not just the ideas but also the language in
which you can express these ideas these mathematical Pioneers worked out techniques where you could start to do arithmetic to truth itself you could then apply tools of mathematics to mathematics mathematics is a tool just
like machines are tools that extend the ability of the human body and allow us to do things our body was unable to do mathematical notation is a tool that allows our minds to explore mathematical Concepts that it could not do
logic is the implication which represents the concept of if then in logic it uses this bit of notation this statement a implies b means if statement a implies b means if proposition a is true then proposition B
is true we can represent how implication works with a truth table if both A and B are true then the implication must also be true as well however if a is true and
B was false then that means that there's something wrong with the implication so the implication must be false how about when a is false well that's the thing about implications like a sneaky Genie they don't tell you anything about the
false case of a so the implication is also true when a is false and B is true also true when a is false and B is true and also if a is false and B is false this truth table looks somewhat familiar as logic became more formalized it
shifted away from using truth tables and started to be be expressed in terms of rules of derivation in this in this more formal approach math is made up of three parts a language that is the symbols and grammar that tells you how the symbols
grammar that tells you how the symbols go together a logic the steps between propositions or more generally how the truth or falsity of one proposition affects the other propositions truthfulness and the axians the starting
truthfulness and the axians the starting point from where our logic grows a formal axionic system or fast for short the most popular fast is zfc with classical logic however it is not the only one oh and a quick tangent this is
why I get so frustrated with mathematical Cooks if you want mathematics to do something like have countable reals or have a distinction between. n repeating and one or whatever else it is totally possible you just
have to come up with a fast that will allow it that mathematical system that you invented might have be even useful or interesting however to do it right requires you to invest the time to
understand how mathematicians communicate and how to formalize communicate and how to formalize mathematical ideas in math to do otherwise would be like attempting to publish a book of Japanese love poems
publish a book of Japanese love poems without knowing any Japanese anyway the most popular alternative to classical zfc is called constructivist mathematics the goal of constructivist mathematics
is that whenever you want to prove that something exists you have to be able to construct it that constructed thing is called a witness because like a witness called a witness because like a witness it stands as evidence of the proof in
constructivist mathematics in order to prove that an Ali squeel exists you would have to show how to create an Ali squeel while in classical mathematics
you could do an indirect proof that an Aly squibble exists for example you could show that if you assume that Aly squibbles don't exist and then use this non-existence to show that some impossible condition results from Ali
squeebles non-existance that proves that Ali squeebles must exist you can't do this style of proof in constructivist logic because constructivist logic lacks the law of excluded middle this classical law is expressed as a is true
classical law is expressed as a is true or not a is true now that sounds a bit obvious if something is not false then it must be true so no matter what the truth of a is one of these two must be true however just because it's obvious
doesn't mean it is correct and a cool thing in mathematics is we can do what what if experiments and explore alternative universes with different Logics in constructivist logic if not not a is true you cannot conclude that a
is true but why would we ever choose such a strange and limiting logic system some do it because they think it better fits what they think mathematics should look like however I think there's a far better reason I am sure you've noticed
that implications and function look very much like each other it turns out that everything in constructive mathematics has a correspondence in type Theory a proposition corresponds to a type A Witness corresponds to a program that
inhabits that type an implication corresponds to function types not a corresponds to function types not a corresponds to a to empty as we will go on we will fill in the rest of this table with other correspondents let's
make a proof using type Theory here is a very common proposition that you will normally have to prove as an assignment in your first logic class this is a very useful property because it allows us to chain together strings of implication
and have them collapse into a single implication what is great about type theory is you can use a technique that I call the typed hole method to create your proof we will start off with a hole which is a to B to B to C to a to c type
along the side I'm going to list all the variables that are in scope currently there are no variables in scope since this is a function type we know that the this is a function type we know that the whole must have an argument of a to B so
let's add that and we will shrink the whole to cover the unused types AB is now added to the list of our available variables now we can repeat the same
variables now we can repeat the same reasoning and get the variable BC again our whole has a function type another argument this time for the type A argument this time for the type A leaving a hole of C now we have to find
leaving a hole of C now we have to find a way to generate an element of type c well there is only one function in scope that will emit a c and that is BC but BC has to be called with an argument of type B which leaves us with this hole
type B which leaves us with this hole but we can get a B from the function ab and we've already have a VAR that Pro provides us with a object of type A so
provides us with a object of type A so here is our program a witness of this proposition thus proving it true how about something more complex well you know how I said that not not a isn't the same as a in constructivist logic well
same as a in constructivist logic well curiously not not not a is the same as not a this is called triple negative elimination and it is something that we can prove even better is an example of something that doesn't seem immediately
obvious let's start with our hole shaped with like the thing we want to prove since the hole is a function type we implement it by declaring an abstraction implement it by declaring an abstraction in this case introducing a iable n okay
now we have another function type so we declare another abstraction for a now the only function we have available that has empty as its return type is the an
has empty as its return type is the an one so we call that and introduce the hole for its argument this hole is another function type so again we can another function type so again we can introduce an abstraction and give it a
new hole oh we've got back to the empty type hole however we now have an as a type hole however we now have an as a VAR in this scope so we can call that now with a hole of a we can fill it in with the argument that we've given and
with the argument that we've given and we have once again proven our result for triple negative elimination even though implication is very powerful in order to have a fully featured system of logic we're going to need something think more
we're going to need something think more so in the next spilling the hot tea video we will be covering the equivalence of and and all product types equivalence of and and all product types and some types so please subscribe for
and some types so please subscribe for that