Set-like mathematics in type theory

[Thomas Kehrenberg]

This is the fourth entry in my series on type theory. We will introduce a lot of notation that is reminiscent of set theory, to make everyone feel more at home, and then we’ll discuss the axiom of choice.

Subtypes

Our next topic is “subsets” within types. I mentioned in the beginning that we can define “subsets” within types via predicates. This usually works great, but sometimes the “subset” needs to be more type-like and then a predicate won’t do.

As an example, say we have the following predicate on the natural numbers

$$even\left(n\right):\equiv \exists (m:N).(n=2\cdot m)$$

with the type $even:N\to \Omega$ (where $\Omega$ represents all truth values). Then in order to claim that $e$ is an even number, we write $even\left(e\right)$. If you were really into using the membership symbol $\in$, then you could also write this as “$e\in even$” and as long as you make clear what is meant by that (namely, $even\left(e\right)$), this is well-defined.

However, we can’t do something like “$\forall (e:even)$” with our predicate, because you absolutely need a type there in the quantifier. So what do we do when we want to quantify over all even numbers?

No problem, we’ll just use the the same trick we used to define the subuniverse $TruthVal$. With a sum type, we can define a type which basically corresponds to the subset defined by the predicate:

$$E:\equiv \sum _{n:N}even\left(n\right).$$

What do the elements of $E$ look like? They are pairs where the first element is a natural number $n$ and the second element is a witness element $p$ for the fact that $n$ is even: $(n,p)$. There can be no $(n,\cdot )$ in $E$ where $n$ is not even because then there wouldn’t be a witness. Likewise, as long as you can prove $even\left(n\right)$ for some $n$ (with witness $p$), then $(n,p)$ is clearly an element of the type. So, the elements of the type $E$ aren’t directly the elements of the subset of even numbers, but there is a very obvious mapping between the two (namely just throwing away the witness). In fact, we will often pretend that the elements of $E$ are just the elements of the subset defined by the predicate. And now we can quantify over the even numbers: $\forall (e:E)$.

Types that have been constructed from some base type in the way we constructed $E$ here from $N$ (i.e., with $\sum$ and a predicate) are called subtypes of the base type. Thus, $E$ is a subtype of $N$. If the base type is a universe $U$, we’ll say subuniverse instead of subtype, but the mechanism is exactly the same.

As this is a common construct, there is a special notation for it, but we only use it if the expression after the $\sum$ symbol is a predicate, i.e., a function that returns a truth value/​subsingleton, $\varphi :A\to \Omega$:

$$\{x:A|\varphi (x\left)\right\}:\equiv \sum _{x:A}\varphi \left(x\right).$$

This is of course simply set-builder notation. With this, we could have defined the subtype $E$ as

$$E:\equiv \{n:N|\exists (m:N).n=2\cdot m\}.$$

Note that in set theory, the axiom of specification is needed to be able to construct subsets from predicates, but in type theory, we can just do it with sum types, as long as we encode logic the way we did. (Another good reason for propositions-as-types.)

Set operations

At this point in the HoTT book, the authors define set operators, like union $\cup$ or intersection $\cap$, on these subtypes, because we want to do all kinds of mathematics and those operators are often very useful. For example, here is how they define inclusion, $\subseteq$:

$$(\{x:A|\varphi (x\left)\right\}\subseteq \{x:A|\psi (x\left)\right\}):\iff (\forall (x:A).\varphi \left(x\right)\Rightarrow \psi \left(x\right))$$

So, a subtype is included in another subtype if the underlying predicate of the first subtype implies the predicate of the second subtype. This definition works because subtypes are backed by predicate functions and so we can define these set operations in terms of operations on predicates.

However, defining these set operations as acting on subtypes seems to me like trying to be a bit too clever. One problem is the type signature of the operators. We could write it like this:

$$\subseteq :\prod _{A:U}Subtype\left(A\right)\times Subtype\left(A\right)\to \Omega$$

but then how to define $Subtype\left(A\right)$ – the type of all subtypes on $A$? I think the definition would be this

$$Subtype\left(A\right)\equiv \{T:U|\exists (\varphi :A\to \Omega ).T=\{a:A|\varphi (a\left)\right\}\}$$

but this does not look like a nice definition at all. This seems like a hint to me that the subuniverse of subtypes is not a natural concept, and we shouldn’t define functions on this abomination.

The second problem I see is that defining these operations on subtypes risks blurring the distinction between types and objects with set-like semantics. For example, you might accidentally use $\subseteq$ on a type which wasn’t a subtype, because it might sometimes be hard to tell the difference.

For these reasons, I would define set-operators (and relations) like “$\subseteq$” on good old predicate functions:

$$\begin{array}{cc}& \subseteq :\prod _{A:U}(A\to \Omega )\times (A\to \Omega )\to \Omega \\ & \varphi {\subseteq }_A\xi :\equiv \forall (a:A).\varphi \left(a\right)\Rightarrow \xi \left(a\right)\end{array}$$

In words: in the domain $A$, property $\varphi$ is a sub-property of $\xi$ if, for all objects in the domain, $\xi$ is true whenever $\varphi$ is true. This definition is concise and easy to read.

The goal is here to make set-like mathematics (which uses relations and operators like $\subseteq$, $\in$, $\cap$, $\cup$) less cumbersome when done on top of type theory. Working with these predicates in type theory should feel as natural as working with sets in set theory.

So, let’s define more set operators and relations. We already mentioned “$\in$” above:

$$\begin{array}{cc}& \in :\prod _{A:U}A\times (A\to \Omega )\to \Omega \\ & a{\in }_A\varphi :\equiv \varphi \left(a\right)\end{array}$$

And as a reminder, we can also write “$P\left(A\right)$” (power set type) instead of “$A\to \Omega$” to make the type signature even more concise.

The following operators return a new predicate, so we have to use anonymous functions to define them (I skipped the type signatures and type subscripts this time):

$$\begin{array}{cc}\varphi \cap \xi & :\equiv \lambda a.\varphi \left(a\right)\wedge \xi \left(a\right)\\ \varphi \cup \xi & :\equiv \lambda a.\varphi \left(a\right)\vee \xi \left(a\right)\\ A\setminus \varphi & :\equiv \lambda a.\neg \varphi \left(a\right)\end{array}$$

As is usual with these operators, we’re writing them in infix notation.

But, as nice as working with predicate functions is, if you want to quantify over elements, you still need a (sub-)type! You have two choices here: $\forall (a:\{a:A|\varphi \left(a\right)\left\}\right).(\cdots )$ or $\forall (a:A).\varphi \left(a\right)\Rightarrow (\cdots )$. Both are formally correct, but we will prefer the latter.

(If I could suggest another notation, it would be this: $A|\varphi :\equiv \{a:A|\varphi (a\left)\right\}$, which reduces the notation to only the essential symbols; such that we can write $\forall (a:A|\varphi ).(\cdots )$, but I’ll try to keep the notation pretty standard here, so I won’t be using this.)

If $S:P\left(P\right(A\left)\right)$ is a predicate on predicates on $A$ (“a set of subsets”), we can also define arbitrary, non-binary intersection and union on it.^[1] For once, I will be pulling out all the stops to make this look like set theory (even though it’s type theory in disguise!):^[2]

$$\begin{array}{cc}\bigcap S& :\equiv \lambda a.[\forall (S:P\left(A\right)).S\in S\Rightarrow a\in S]\\ \bigcup S& :\equiv \lambda a.[\exists (S:P\left(A\right)).S\in S\wedge a\in S]\end{array}$$

and don’t panic – the square brackets $[\cdots ]$ mean exactly the same as round brackets $(\cdots )$. It was just getting a bit hard to parse with only round ones.

There are other beloved set theory notations that can be “rescued” by giving them new semantics in type theory. For example, if you have $a,b,c:A$ then you could write $\{a,b,c{\}}_A$ to refer to the subtype $\{x:A|(x=a)\vee (x=b)\vee (x=c\left)\right\}$. But I will stop here now.

To summarize again the difference between subtypes and predicates: if you’re working in a fixed base set (like $N$ or $R$) and you want to use set-like operations, use predicates; if you are in a context where a type is needed or you only expect to do “type-level operations” (like quantifying over elements), use subtypes. In the following, we will see many examples where subtypes are very useful.

Construction of other numbers

Mathematicians don’t only want to work with boring old natural numbers, so with the power set type and subtypes in hand, we can also construct other numbers, like the integers $Z$ and the rational numbers $Q$. They can be defined as equivalence classes on binary product types like $N\times N$. I’ll be very brief in this section; it’s mostly just to show that it’s possible.

So, let’s first define equivalence classes. If $A$ is some base type and $R$ is a relation on $A$ with type $A\times A\to \Omega$, then the equivalence classes of $R$ belong to the following type (which is also called the quotient of $A$ by $R$) :

$$A/R:\equiv \{S:P(A\left)|\exists \right(a:A).\forall (b:A).R(a,b)\iff b\in S\}.$$

(I wrote “$b\in S$” here to mean “$S\left(b\right)$”.) As you can see, this is a subtype of the power set of $A$. Each element of $A/R$ is one equivalence class, which is a “subset” of $A$ whose members are related according to $R$.

For the integers $Z$, we define a relation on the product $N\times N$ with the following definition:

$$diff\left(\right(a,b),(x,y\left)\right):\equiv (a+y=x+b):(N\times N)\times (N\times N)\to \Omega$$

such that

$$Z:\equiv (N\times N)/diff$$

where we can choose the canonical forms $(n,0)$ and $(0,n)$ for the equivalence classes, corresponding to $+n$ and $-n$ respectively.

To get from the integers to the rational numbers, we take $Z\times N$ and use this relation:

$$ratio\left(\right(a,b),(x,y\left)\right):\equiv (a\cdot (y+1)=x\cdot (b+1)).$$

The $+1$ is there to prevent division by zero; we could have also just used the natural numbers without 0 instead. With this we have

$$Q:\equiv (Z\times N)/ratio.$$

A pair $(a,b):Q$ corresponds to the fraction $a/(b+1)$. The canonical form of a rational number is a fraction that can’t be reduced any further (“fraction in lowest terms”) – every rational number has a unique representation as an irreducible fraction with a positive denominator.

Constructing the real numbers is a bit more involved but it basically works like it usually does; for example via Dedekind cuts, which we can represent by two predicates on $Q$. So, let $L$ and $U$ be two predicates (aka “subsets”) on $Q$. Then if $isCut(L,U)$ is a predicate that tells us whether the pair $(L,U)$ is a Dedekind cut (you can look up the definition on Wikipedia), then the (Dedekind) reals are given by the following:

$$R_{Dedekind}:\equiv \{(L,U):P\left(Q\right)\times P\left(Q\right)|isCut(L,U)\}.$$

The usual operations and relations for the real numbers (e.g., $<$ and $\le$) can then be defined on this type.

We can also define restrictions like $R_{>0}$, the positive real numbers, by defining a subtype with a predicate like $\lambda x.(x>0)$. The very common “$\forall \epsilon >0$” from calculus can then be written as $\forall (\epsilon :R_{>0}$), but I suppose you could also write $\forall (\epsilon >0:R)$.

The family of finite types

To round out this section on numbers, I’ll quickly comment on a type family that I’ve already briefly mentioned before: the family of finite types. As a reminder, a family of types is a type-valued function from some index set $I$ to some types: $I\to U$. A very simple type family $B$ with the index set $2$ would be, for example, $B\left(0_2\right):\equiv R$, $B\left(1_2\right):\equiv Q$.

The family of finite types is indexed by $N$ and can be defined like this:

$$\begin{array}{cc}& Fin:N\to U\\ & Fin\left(n\right):\equiv \{m:N|m<n\}\end{array}$$

The essential point is that $Fin\left(n\right)$ has exactly $n$ elements. And if $A\simeq B$ means that types $A$ and $B$ are equivalent/​isomorphic (see the next post for a rigorous definition of that), then of course we’ll have^[3]

$$\begin{array}{cc}0& \simeq Fin\left(0\right)\\ 1& \simeq Fin\left(1\right)\\ 2& \simeq Fin\left(2\right)\end{array}$$

The type family $Fin\left(n\right)$ is very useful when you want to iterate over a finite index. For example, instead of

$$\forall (i:N).(i<n)\Rightarrow (\cdots )$$

you can just write

$$\forall (i:Fin(n\left)\right).(\cdots )$$

The family of finite types is generally very handy for indexing things; for example other type families: $B:Fin\left(10\right)\to U$. However, finite types can also be used to index vectors! Now, usually, vectors are realized as tuples, like $v:R\times R\times R$ (or $v:R^3$), but there are some advantages to realizing vectors as “functions” on finite types, $v:Fin\left(3\right)\to R$. Vector entries are then accessed by function application, $v\left(0\right)$, where $0:Fin\left(3\right)$. This is how the dex programming language formalizes arrays, for example. (Though these “array functions” are memoized for performance.)

The advantage is that it allows you two write functions that work with generic vector sizes while still being type-safe (or rather, shape-safe). For example, a concatenation function $concat$, which concatenates two vectors of arbitrary length, would have the following type:

$$concat:(I\to R)\times (J\to R)\to \left(\right(I+J)\to R)$$

where $I$ and $J$ are arbitrary index types and $I+J$ is the binary sum type. If we now pass in two vectors, $u:Fin\left(2\right)\to R$ and $v:Fin\left(4\right)\to R$, then the result has the type $\left(Fin\right(2)+Fin(4\left)\right)\to R$, which isn’t quite $Fin\left(6\right)\to R$, but the two types are isomorphic. So, we can read off from the types that the result is a vector of length 6.

More examples of subtypes

When we introduced sum types, we used the type of all groups as an example. The type we gave was

$$Group\equiv \sum _{T:U}(T\times T\to T)\times T$$

but we can actually be more precise than that. As this definition is written, an element of $Group$ is just a type with some binary operation and some element, but those do not necessarily satisfy the group axioms! For example, in a group, the binary operation needs to be associative and the special element needs to be a neutral element (with respect to the binary operation), but the type doesn’t guarantee that! To solve this, we can filter for those elements that satisfy the group axioms with set-builder notation:

$$Group:\equiv \{(T,\ast ,e):\sum _{T:U}(T\times T\to T)\times T|isGroup(T,\ast ,e)\}$$

where

$$\begin{array}{cc}isGroup(T,\ast ,e)& :\equiv assoc(T,\ast )\wedge neutr(T,\ast ,e)\wedge inv(T,\ast ,e)\\ assoc(T,\ast )& :\equiv \forall (a:T).\forall (b:T).\forall (c:T).((a\ast b)\ast c=a\ast (b\ast c))\\ neutr(T,\ast ,e)& :\equiv \forall (a:T).((e\ast a=a)\wedge (a\ast e=a))\\ inv(T,\ast ,e)& :\equiv \forall (a:T).\exists (b:T).((a\ast b=e)\wedge (b\ast a=e))\end{array}$$

(As usual, the binary operation is written in infix notation.) Technically, an element of this new $Group$ type will not be the triplet $(T,\ast ,e)$, but the 4-tuple $(T,\ast ,e,p)$ where $p$ is the witness for $isGroup(T,\ast ,e)$, but, again, we’ll usually ignore this.

If you now want to make statements about an arbitrary group, you can just say, “let $(G,\ast ,e):Group$” and then derive clever things about $G$.

As another example of subtypes, consider the type of continuous functions between $X$ and $Y$. The plain function type is $X\to Y$, but if we have a predicate $iscont\left(f\right)$ which tells us whether function $f$ is continuous, then we can narrow down the type:

$$Cont(X,Y):\equiv \{f:X\to Y|iscont(f\left)\right\}.$$

$Cont$ is then a type family indexed by $X:U$ and $Y:U$. Of course, if the definition of “continuous” is clear from the context, then you can just informally write

$$Cont(X,Y)\equiv \{f:X\to Y|f\text{is continuous}\}$$

Axiom of choice

As mentioned before, the law of excluded middle (LEM) is actually implied by the (type-theoretic version of the) axiom of choice. So, let’s talk about it!

In set theory, one common way to state the axiom is this:

For any set $X$ of nonempty sets, there exists a choice function $f$ that is defined on $X$ and maps each set $S\in X$ to an element of that set $S$.

As always, a set is a predicate in our theory. So, for a set of sets, we need multiple predicates – a family of predicates.^[4] We can index those predicates with an index type $I$. If the predicates are on the type $A$, then the indexed predicates are given by

$$\varphi :I\to A\to \Omega ,$$

a function $\varphi (i,a)$ with two parameters (we used currying): an index $i:I$ (to index the predicate) and an element $a:A$. This may look more like a relation than a predicate, but the first element is really only there for indexing; we could also write it as “${\varphi }_i\left(a\right)$” (or even “$a\in {\varphi }_i$”) instead of $\varphi (i,a)$ (but $\varphi (i,a)$ is more standard, so we’ll use that).

So, $\varphi$ plays the role of the set of sets – $X$ in the above definition. Now, how to ensure the sets are nonempty? We will need to assume $\forall (i:I).\exists (a:A).\varphi (i,a)$; for all indices $i:I$, there exists an $a:A$ such that the predicate holds.

Finally, what is the thing we want to assert? The existence of a function $f$ which takes an index $i:I$ and returns an element of $A$ for which the predicate holds:

$$(\forall (i:I).\exists (a:A).\varphi (i,a))\Rightarrow (\exists (f:I\to A).\forall (i:I).\varphi (i,f(i\left)\right))$$

Translated: “if all the sets in the family $\varphi$ are non-empty, then a function $f$ exists, which, for all sets in the family, picks an element of the set.”

However, we can make this slightly more general by allowing that the sets don’t all need to come from the same base type $A$. So, one set could be from $N$ and another from $R$ but there should still be a choice function that picks an element from all of these. In order to allow this, we have to replace the fixed type $A$ with a type-valued function $A\left(i\right)$ that may return different types based on the value of $i$. Then we get:^[5]

$$AC:\equiv (\forall (i:I).\exists (a:A\left(i\right)).\varphi (i,a))\Rightarrow (\exists (f:\prod _{i:I}A\left(i\right)).\forall (i:I).\varphi (i,f\left(i\right)))$$

where all the $\varphi (i,a)$’s are subsingletons. We can see that $f$ needs to belong to a dependent function type in this more general setup.

And that’s the axiom of choice transcribed to type theory! As with the axiom of choice in set theory, for finite index types $I$ this is actually a theorem that can be proved. (Finite types are those types where an equivalence exists between the type and a member of the family of finite types, $Fin\left(n\right)$, for some $n$. We’ll define “equivalence” later on.) The axiom is only needed for infinite $I$.

So, let’s prove the axiom of choice for the case where $I$ is the unit type $1$ (i.e., it’s very much finite), because we can learn something from that. In this case, we don’t really need to index $\varphi$ and so we can just write

$$(\exists (a:A).\varphi \left(a\right))\Rightarrow (\exists (f:1\to A).\varphi (f(\star )))$$

Now, with “classical” reasoning, this is easy to prove: if there exists an element in $A$ that is in $\varphi$, then let $a$ be such an element; next, we’ll just define the constant function $f\left(x\right)\equiv a$; surely we’ll then have $\varphi \left(f\right(\star \left)\right)$.

But let’s check how this works with the underlying types:

$$\Vert \sum _{a:A}\varphi \left(a\right)\Vert \to \Vert \sum _{f:1\to A}\varphi (f(\star ))\Vert .$$

It kind of looks like we are given the pair $(a,p)$ where $a:A$ and $p$ is the witness for $\varphi \left(a\right)$, and then it seems like we can again construct $f$ as the constant function $\lambda x.a$ and use $p$ as the witness for $\varphi \left(f\right(\star \left)\right)$.

However, we don’t actually get the pair $(a,p)$; we only get the double negation of it: $\parallel \dots \parallel$ and we can’t apply DNE to this because the inner type might not be a subsingleton. So what can we do?

To be clear, the “classical” proof above is correct. But in order to understand why it is correct in the underlying type system, we’ll need to understand more about the operation we wrote as $\parallel \dots \parallel$. We implemented this with double negation, but there are actually other ways to do this, and so this operation has a more general name: propositional truncation. It is called that because it “truncates” a type to a subsingleton, which are used for propositions. We will later get to know other truncations as well.

Propositional truncation in detail

The core properties of propositional truncation are these:

1. If some type $A$ is inhabited, then so is $\parallel A\parallel$. Furthermore, $\parallel A\parallel$ is a subsingleton.

2. If $A$ is a subsingleton, then $A$ is inhabited if $\parallel A\parallel$ is inhabited.

3. If $P$ is a subsingleton and we have a function $f:A\to P$, then there exists a function $g:\parallel A\parallel \to P$ such that $g\left(\tilde{a}\right)=f\left(a\right)$ for all $a:A$ (where $\tilde{a}$ is the singular element of $\parallel A\parallel$).

The third property means that if the inhabitedness of $A$ can prove the proposition $P$, then the inhabitedness of $\parallel A\parallel$ is already sufficient to prove it. This is very powerful. It means that if you know some $\parallel A\parallel$ is inhabited, and you want to prove the proposition $P$ (which is a proper subsingleton), then you may just assume you have an element of $A$ and if that’s enough to prove $P$, then $P$ also follows from just $\parallel A\parallel$. This is a way to actually prove things from $\parallel A\parallel$.

So, let’s convince ourselves that double negation (with LEM/​DNE as an axiom) actually satisfies these properties. We already showed properties 1 and 2 when we introduced the notation $\parallel \dots \parallel$, so we only need to show property 3. This will be the last real proof in this series.

So, say $P$ is a subsingleton and we have an $f:A\to P$. Our goal is to construct $g:\parallel A\parallel \to P$. As a reminder:

$$\parallel A\parallel \equiv (A\to 0)\to 0.$$

We cannot apply DNE to this because $A$ might not be a subsingleton. In order to construct $g$, we will first construct $h:\parallel A\parallel \to \parallel P\parallel$, because we can easily get $g$ from this via property 2 (i.e., just apply DNE to $\parallel P\parallel$). Expanding the propositional truncation, the type of $h$ is:

$$h:((A\to 0)\to 0)\to (P\to 0)\to 0.$$

If you look carefully at that type and also consider the type of $f$, you can come up with the following:

$$h(\check{a},\overline{p}):\equiv \check{a}(\overline{p}\circ f)$$

where “$\overline{p}\circ f$” is the function composition of $\overline{p}$ and $f$, defined like this:

$$\begin{array}{cc}& \circ :\prod _{X:U}\prod _{Y:U}\prod _{Z:U}(Y\to Z)\to (X\to Y)\to (X\to Z)\\ & f\circ g:\equiv \lambda x.f(g\left(x\right))\end{array}$$

We then get $g$ by composing $h$ with $dne:DNE$, the double-negation-elimination function (for the type $P$):

$$g:\equiv {dne}_P\circ h\equiv {dne}_P\circ (\lambda \check{a}.(\lambda \overline{p}.\check{a}(\overline{p}\circ f))).$$

What’s left to show is that $\forall (a:A).g\left(\tilde{a}\right)=f\left(a\right)$. But this is trivial because both $g\left(\tilde{a}\right)$ and $f\left(a\right)$ are in $P$ and $P$ is a subsingleton where all elements are equal to each other. So, this proves property 3 for the truncation based on double negation.

Axiom of choice for a single set

Now that we have a better understanding of propositional truncation, let’s look again at our very finite (single set only) axiom of choice:

$$\Vert \sum _{a:A}\varphi \left(a\right)\Vert \to \Vert \sum _{f:1\to A}\varphi (f(\star ))\Vert$$

According to property 3 of propositional truncation, we may actually prove this instead:

$$\left(\sum _{a:A}\varphi \right(a\left)\right)\to \Vert \sum _{f:1\to A}\varphi (f(\star ))\Vert$$

This in turn is implied by

$$\left(\sum _{a:A}\varphi \right(a\left)\right)\to \sum _{f:1\to A}\varphi (f(\star ))$$

because by property 1 of propositional truncation, $A$ always implies $\parallel A\parallel$.

So, we may use our naïve proof from above after all: From $(a,p)$ we can construct an element of the codomain like this: $(\lambda x.a,p)$. It’s then left to show that $p$ is actually an element of $\varphi \left(f\right(\star \left)\right)$. By the rules of function application, $f(\star )$ is replaced by $a$, so $\varphi \left(f\right(\star \left)\right)\equiv \varphi \left(a\right)$, which concludes the proof.

In order to prove the axiom of choice for other finite sets, we can use induction over $N$.

I’ll leave it to you to think about why this proof fails for infinite index types.

Proving LEM/​DNE from AC

The proof showing that the axiom of choice implies LEM/​DNE is quite complicated so we’ll only discuss the requirements here. In addition to the axiom of choice, the proof also requires propositional extensionality and function extensionality which we’ll discuss in the next article.

One tricky aspect is that we of course can’t assume LEM/​DNE for the proof (because that’s what we’re trying to prove) so we can’t use double negation to implement the propositional truncation that is necessary to formulate the axiom of choice. One possible solution to this problem is to simply assume a propositional truncation operation with the 3 necessary properties, as an additional part of our type theory, simply as a black-box operation.

Another solution is to use the following for propositional truncation:

$$\parallel A\parallel :\equiv \prod _{V:\Omega }((A\to V)\to V)$$

however, this only works if the set $\Omega$ exists – the set that indexes all truth values/​subsingletons. We mentioned before that $\Omega$ is guaranteed to exist under LEM+propositional extensionality, but, again, we can’t assume LEM, so we would instead need to explicitly assume the existence of $\Omega$ as an axiom for this encoding to work.

As we will later encounter other truncations though, I think it makes most sense to simply assume propositional truncation as an additional element of type theory.

Finally, is there some intuition for why AC (axiom of choice) would imply LEM? Well, you could actually view LEM as a sort of mini-AC. AC allows you to pick an element as long as you can prove that there are elements there (i.e., that the subsets are all non-empty). And similarly, LEM/​DNE allows you to pick an element of $A$ as long as you can prove that $A\to 0$ is not inhabited. In a way, both allow you to conjure up an element out of nothing, as long as you have sufficient reason to believe that an element exists.

---

In the next and final installment of this series, we will, at last, find out what the deal is with extensionality. We will also discuss the celebrated univalence axiom.

1. ^

   We can also define these for an indexed family of predicates, $S:I\to P\left(A\right)$:

   $$\bigcup _{i:I}{S}_i\equiv \lambda a.\exists (i:I).a\in S_i$$

   and similarly for intersection.

2. ^

   Note that if $S$ is “empty” (i.e., false everywhere), then the intersection of it will be all of $A$, which might not be what you want. So make sure $S$ isn’t empty!

3. ^

   Why use $Fin\left(2\right)$ when you can just use $2$? The problem with the “$2$” notation is that it stops working for higher numbers, like $Fin\left(100\right)$. I think “$100$” would be very confusing as a type.

4. ^

   Why not a predicate of predicates? Because we later want to allow the predicates to live in different base types, which you can only express with a family. And anyway, you can turn a predicate of predicates $\Psi :(A\to \Omega )\to \Omega$ easily into a family of predicates; just use the corresponding subtype, $I\equiv \{\varphi :A\to \Omega |\Psi (\varphi \left)\right\}$, as the index type. The family is then given by the function $\xi \equiv \left(\lambda \right(\varphi ,p).\varphi )$ where $p$ is the witness for $\Psi \left(\varphi \right)$.

5. ^

   You could call this the “truncated version” of the axiom of choice in type theory because “$\exists$” gets translated to $\parallel \sum \dots \parallel$. The “untruncated version” with plain sum types $\sum$ is a theorem in type theory.

[Slider]

Practising expressing old interests in a new language:

$S=S_{form}/{\le }_{Sf}$

$S_{bucket}=P\left(S\right)$

$S_{form}=a:S_{bucket},b:S_{bucket}|numeri{c}_S(a,b)$

$pair\left(a\right):S_{form}\to S_{bucket}\times S_{bucket}$

$numeri{c}_S(a,b)=\forall x(x\in a(\forall y{\le }_{Sb}\left(pair\right(x),pair(y\left)\right)\left)\right):S_{bucket}\times S_{bucket}\to \Omega$

$firstborn\left(a\right):S\to S_{form}$

${\le }_{Sf}(a,b)={\le }_{Sb}\left(pair\right(a),pair(b\left)\right):S_{form}\times S_{form}\to \Omega$${\le }_{Sb}(a,b,c,d)=\neg \exists x(x\in a\wedge {\le }_{Sn}(c,d,x\left)\right)\wedge \neg \exists y(y\in d\wedge {\ge }_{Sn}(a,b,y\left)\right):S_{bucket}\times S_{bucket}\times S_{bucket}\times S_{bucket}\to \Omega$

${\le }_{Sn}(c,d,x)={\le }_{Sb}(c,d,pair(firstborn\left(x\right)\left)\right):S_{bucket}\times S_{bucket}\times S\to \Omega$

${\ge }_{Sn}(a,b,y)={\le }_{Sb}\left(pair\right(firstborn\left(y\right)),a,b):S_{bucket}\times S_{bucket}\times S\to \Omega$

It is a known system and a terribly recursive one. One can get going by the fact that $\varnothing \in P\left(A\right),A\in U$