[00:03] introduced the product sum and equality types, the type theory equivalents to and, or, and equals. However, when introducing them, I kept running into problems where I needed to be able to work with not just a fixed finite
[00:20] collection of propositions, but an unfixed, possibly infinite collection of types. In this video, we are going to take that next step, that step into the infinite. I'm going to introduce type families and universes, which are a way
[00:37] of collecting types together for a common purpose. Then, I'm going to show a few ways we use type theories, I types, which extend product types, and
[00:51] types, which extend product types, and sigma types, which extend sum types. Then, finally, in this video, I'm going to talk about the natural or counting to talk about the natural or counting numbers, which is, in a way, the
[01:04] simplest infinite type and a great way to show how these things work.
[01:16] Up to now, we have been dealing with functions which act on elements within types. In type theory, everything is an element of a type, including types themselves. So, we can have a function
[01:29] which goes from elements within a particular type to elements which are particular type to elements which are types themselves. This gets denoted like types themselves. This gets denoted like this. I tend to call the domain of a
[01:41] this. I tend to call the domain of a type family function that family's type family function that family's index. The fancy-looking U stands for universe. A universe is the type of types, which is inhabited by almost all
[01:56] types, which is inhabited by almost all the types. Since a universe is a type of types, does that it mean it inhabits the universe itself? No. If you have a a universe which inhabits itself, you get
[02:12] paradoxes. Paradoxes in type systems lead to false proofs in type systems. An automated validator using that type system would falsely validate that
[02:24] system would falsely validate that system as being correct. If we used that system as being correct. If we used that for a safety critical computer program, it would be marked as correct when it's not. That program could allow
[02:36] incompatible chemicals to mix, resulting in the release of toxic gas, polluting the air. All die. Oh, the embarrassment. One way of avoiding this tragic outcome
[02:49] is if we have a rule that the universe isn't allowed to contain itself, but isn't allowed to contain itself, but instead we have a bigger universe containing the smaller universe. Sort of a layered structure, like a matryoshka
[03:03] a layered structure, like a matryoshka doll or an ogre. To keep everything organized, we distinguish between each universe with a subscript. The lowermost universe gets the subscript zero, and each universe goes up one subscript
[03:18] more. But for the most time, we just ignore all of that, use U without a subscript to mean whatever universe makes this work. makes this work. Type families serve a few important
[03:31] purposes. It can be used to collect together types which have some sort of commonality. For example, the first video of this subseries defined the empty type and the unit unit type. You
[03:46] would be able to correctly guess that there is a Boolean type, a ternary type, there is a Boolean type, a ternary type, and so on. We have one of these finite types for every counting or natural number, and we can express this
[04:00] relationship as this function. Now, this function spits out the appropriately function spits out the appropriately sized types for whatever counting number you apply to it. And yes, the natural numbers are going to be defined later on
[04:15] in this video. Another use of type families is a way to do predicate. If something is true about an element of a function, it spits out an inhabited type, and if it isn't, then it spits out an uninhabited type. For example, you
[04:32] could do something like this, where the function will return an inhabited type if the number is even, but return un- but return an uninhabited type but return an uninhabited type otherwise. This directly relates to the
[04:47] next way type families are going to be used, pi types. Product types are great when you want to say two things are true, even when you want to say three say that something is true for an infinite
[05:04] amount of types? That's when dependent function types come in handy, also called pi types. This extends product types into an unfixed or infinite family
[05:17] of elements. This extends product types into unfixed or infinite elements. It is into unfixed or infinite elements. It is type theory's equivalent to for all. Here is how it is typically denoted. Underneath the pi, it defines a new
[05:32] variable and sets it to be a particular type. Inside the scope of that pi, the variable is used as an argument to a type family. A pi type is inhabited if
[05:45] for all elements of a given index type, the family returns an inhabited type. So, in other words, the predicate is true for every element of the index
[05:57] type. If you think about product types as being inhabited by tuples, then pi types are inhabited by empty tuples consisting of witnesses for every
[06:09] element of the index type. Example time. This is the rather trivial statement for every element in a type, that element is equal to itself. Since
[06:23] this is true for every type, we could extend it like this, but which can be extend it like this, but which can be interpreted as saying for every type every element in that type is equal to itself. While being true, it
[06:38] isn't particularly groundbreaking to be honest. So, how do we ensure a pi type is inhabited? That's where induction comes in. Not the type of induction that
[06:50] warms your cooking or that you have to do as part of OSHA training, but mathematical induction. Each index type has an induction which tells you how to create a pi type based on it. We will be showing examples of how to
[07:07] induction when we start to talk about the natural numbers again. Sigma types, but before that, we are going to be talk about dependent pair types, otherwise about dependent pair types, otherwise known as sigma types. Just like pi types
[07:21] extend sum types into the infinite, they have a very similar notation. With sigma types, just one family member of this family has to be inhabited in order for
[07:33] the type to be inhabited. It is inhabited by a pair of the index and the inhabited by a pair of the index and the witness for that particular witness for that particular index. Creating proofs for sigma types
[07:47] is relatively easy because you just have to find the single situation where they work. So, a super trivial example is just fine. For example, for this
[07:59] particular sigma type, you would just have to show it is inhabited by the pair of two raffle. Now, we have sigma types and we raffle. Now, we have sigma types and we have pi types. We can formally write the
[08:13] uniqueness principle for the rational numbers, which we discussed in our previous video, which says if there exists a pair of numerators and denominators that are equal after multiplication, then they are
[08:27] propositionally equal. Let's go over this statement to understand how each part works. The first pi introduces our numerator and denominator and says
[08:39] that we will be examining all the the domain of rational numbers. The second pi introduces our second pair that we will be comparing to. Then we have our function type. Recall that function types can act as an
[08:55] if-then clause in logic. So, let's look at the if clause. We have a sigma type, at the if clause. We have a sigma type, which introduces Q, a whole number integer variable. Because it is a sigma type, it only needs to be true for at
[09:12] type, it only needs to be true for at least one of the whole numbers. And we have a product type, which we established in our previous video, corresponds to an and. So, this becomes populated when both sides are populated.
[09:28] On the first part of our product type, we multiply Q by itself, and then we compare to see if it's greater than or equal to one. This is a roundabout way of saying non-zero, but in a more positive, encouraging way. Without
[09:43] positive, encouraging way. Without double negative elimination, saying not double negative elimination, saying not equal to zero can cause problems and being sort of positive and avoiding saying not is a way to do this more
[09:58] non-problematically in constructivist ways. In the second part of our product type, we multiply both of our product type, we multiply both the denominator and the numerator of the
[10:11] pair by Q. If there exists some Q that makes these two sides equal, then this will be true. With that, we go to the other side of the type, which asserts,
[10:25] since the if clause is true, then that requires the then clause to be then that requires the then clause to be true. So, the equality type will be true. So, the equality type will be populated by this rule. By the way, my
[10:38] previous definition of rationals in my previous video, I introduced a mistake. I forgot to use a denominator type, which excludes zero. Also, there is another way you could do
[10:53] Also, there is another way you could do rationals via multiplication. You get rationals via multiplication. You get this type as your uniqueness rule, which asserts that rationals are equal when
[11:05] the left numerator times the right denominator equal right numerator times the left denominator.
[11:18] does have the disadvantage that it doesn't allow me to show a use of sigma types with it. The natural numbers. Okay, we have defined the basic components of logic. And in in of product types, or in the form of sum
[11:33] product types, or in the form of sum types. Pi types for for all and sigma types. Pi types for for all and sigma types for there exists. However, that isn't really useful. To be useful, we will need to be able to do arithmetic in
[11:46] our system. Historically, mathematics started to count livestock and grain. So, let's go back to those ancient roots and define the counting or ancient roots and define the counting or natural numbers. We start with our
[12:01] constructors, zero and succ. I'm pretty sure you're zero and succ. I'm pretty sure you're familiar with what zero is. Succ is an injective function which takes a natural number and constructs the next number.
[12:15] number and constructs the next number. So, succ zero is one. Succ n by definition is going to be one more than n. The nat type ends up populated like this. You will notice that there are basically two kinds of natural numbers,
[12:31] basically two kinds of natural numbers, zero and numbers which are successors. This gives us a very powerful framework for dealing with natural numbers, primitive recursion. In my lambda calculus video, I introduced general
[12:46] calculus video, I introduced general recursion and showed how it can be super dangerous. The type of danger that introduce carelessly into a type system could lead to contradictions. Contradictions that lead to false
[13:00] proofs. False proofs that allow automated verification software to automated verification software to mistakenly misidentify a red light traffic signal as being safe. A traffic signal causing a truck crash. The
[13:13] resulting traffic jam gridlocks the city. The economic loss triggers a collapse in the global economy and inescapable spiral of poverty. Everybody
[13:25] dies. Oh, the embarrassment. However, primitive recursion is far tamer. In primitive recursion, we have a base value, which is returned when the when
[13:37] the argument is zero. Then, we have a step function. The step function tells successor of an argument based on
[13:50] of an argument based on that number and the result of applying the function to that argument. For example, here is a function that adds three to every number. We solve the base case, returning three. And for the
[14:04] successor, we just use the first argument, which gives us the predecessor. We call the successor four times on it, and that gives us the times on it, and that gives us the correct result for add three. To double
[14:17] a number, we have a similar application. For zero, we simply return zero. And for our step function, we simply take the result of the previous function
[14:29] and apply the successor function twice. Even factorial is easy to express. You will notice that with primitive recursion, for every for any value, you
[14:42] only have a finite count of steps to produce a result. This is unlike general recursion, where there is a potential possibility to have an unbound
[14:54] possibility to have an unbound count of steps. Indeed, the rules about count of steps. Indeed, the rules about there being a hierarchy of universes forbids a function from taking itself as an
[15:06] argument. So, we cannot do general recursion, and that keeps us safe from these dangers. And now, we get to talk about the induction principle for
[15:18] natural numbers. Is it possible to have a parasocial relationship with an abstract concept? Because honestly, I have a rather one-sided, unrequited love
[15:30] for induction on the countables. Induction is the way in constructive logic that we can prove the case for all. Informally, we prove it by giving a
[15:45] witness for the base case and then a witness for if given a proof and then a witness for if given a proof for the nth case, produce a proof for the successor of the nth case. And induction will take care of the rest. If
[16:00] we are asked for any witness, then induction will act as a little engine and produce a chain of witnesses starting from the base case and incrementing up to the number that we need a proof for. So, induction is our
[16:16] manufacture a proof for any counting number. And in broader senses, for every inductive type in type theory, we are given a little engine that allows us to produce a proof for all, long as where
[16:33] produce a proof for all, long as where we give the relevant witnesses that that we give the relevant witnesses that that that particular induction requires. And with that, we have introduced enough type theory to be useful for doing most
[16:48] of the mathematics that I'm interested in. But, at the same time, we have just barely scratched the surface of type theory. We have unlocked some of the theory. We have unlocked some of the nodes in my type theory tech tree. And
[17:03] in my next math videos, we'll be exploring some of these nodes that we've exploring some of these nodes that we've unlocked. Now, I can do things like explain Wells' fixed point theorem. I can start on the homotopy bit of
[17:19] can start on the homotopy bit of hot tea, how computable reals so wild hot tea, how computable reals so wild and so well-behaved at the same time, and on all sorts of other wonderful things. I'll even be able to talk about
[17:32] the dangerous forbidden extensions to type theory. So, please subscribe for that and for when I take other brief diversions into
[17:44] other topics that catch my interest. I hope to see you there.