- Family of Types
- “Axiom” (Theorm) of Choice
- Natural Numbers
- Identity Type
- Function Extensionality / Principle of Extensionality

# Family of Types

Family of types is a generalization of the concept of a predicate/relation.

Formally, given a type $A:U$ in a universe of types $U$, one may havea **family of types**
$B:A\rightarrow U$, which assigns to each term $a:A$ a type $B(a):U$. We say that the
type $B(a)$ varies with $a$.

e.g.

the following proposition

is a predicate / propositional function / a family of types (indexed by ) / fibration. We can rewrite it as

The idea is that we are exhibiting a family of types/proofs in that if you give me any particular choice of number, it’s going to give me back a proposition, which may or maynot be inhabitied, but they are all types.

For example, will be uninhabited, and will be inhabitited.

## Some Notations

means $\Gamma$ being a context.

means definitionally equivalent context.

means we have a family of types named $A$ indexed by elements of $\Gamma$

means we have a family of types named $B$ indexed by $x$, which are elements of type $A$ (sometimes subscript $x$ might be omitted)

means definitionally equivalent families of types.

means we have an element of the type

means definitionally equivalent elements of that type

## Functionality / Respect for Equality

Here is the basic idea:

Some important points:

Functionality condition says more:

In other words, if I give you definitionally equal instances, they they are going to be definitionally equal types.

## $\Pi$ and $\Sigma$ Types

$\Pi$ and $\Sigma$ types are both families of types.

$\Pi$ types are a list of types, where each type is a function mapping from one type to another type.

Formation of $\Pi$ ($\Pi-F$):

Introduction rule ($\Pi-I$):

Elimination rule ($\Pi-E$):

$\Pi$ Computation / Equivalence rule ($\Pi-C$):

$\Sigma$ types are a list of indexed pair, where the first term is any type, and the second term is a function of the first term.

Formation of $\Sigma$ ($\Sigma-F$):

Introduction rule ($\Sigma-I$):

Elimination rule ($\Sigma-E$):

Equivalence rule:

# “Axiom” (Theorm) of Choice

Every total binary relation contains a funtion, where a total relation means:

So the axiom of choice in set theory, where $f$ is the choice function:

In type theory, it is actually a therom:

We can write the proof:

Explanation: first it’s clear that what we want to proof is a map from left to right. Let’s explain what’s the types left and right and what should be the instance of those types.

Left: the outer most is a $\Pi$ type of $A$ and something else, and we have $t$ the instance of left type. So $t$ must be a function mapping from $A$ to something. So we go one level deeper, it’s a $\Sigma$ type. An instance of it must be a tuple, where the first term is type $B$, the second term is a mapping from $B$ to $R$. So $t$ is a mapping from $A$ to a tuple.

Right: the outer most is a $\Sigma$ type, so an instance of it is a tuple. The first term is a mapping from $A$ to $B$, the second term is an instance $\Pi$ type. So it should be a function mapping from $A$ to $R$.

Therefore, our outer most $\lambda$ should return a tuple, and each term of it should be a function mapping from $A$ to something. If we apply $t$ to $x$, we get a tuple, or an instance of $\Sigma$ type. We can now apply elimination rules to it. $\Pi_1$ would give us type $B$, and $\Pi_1$ would give us $[\Pi_1(tx)/y]R(x,y)$, which is what we want.

# Natural Numbers

Introduction rules:

():

():

Elimination rules:

- Computational/non-dependent “Godel’s T”

where $rec$ has the following definition:

- Proof by induction / dependent

or

where $rec$ has the following definition:

# Identity Type

Identity formation ($Id_A-F$):

It is a type of proofs that $M$ and $N$ are equal(?) elements of type $A$.

($Id_A-I$):

It is the least reflexive relation, meaning that that’s the only rule we have for identiy, $refl$ is the only thing we can have eventually.

Elimination rule:

Side Note: and any others that
“construct” the “$C\ type$” like things is also called **motive**.

Computation rule:

- Equality is Symmetric

define $sym$ such that ($sym(x)$ can also be written as $x^{-1}$):

Proof:

We use the motive: for $J$, corresponding to $x,y,z,C$ in the above elimination rule motive:

- Equality is Transitive

find such that where $trans(x,y)$ is just like composition $y\cdot x$.

Proof:

We use the motive: for $J$, corresponding to $x,y,z,C$ in the above elimination rule motive:

- Substitutivity/Functionality/Transport

Proof:

We use the motive: for $J$, corresponding to $x,y,z,C$ in the above elimination rule motive:

- Respect

## Therom[Martin-Lof]

If $P:Id_A(M,N)$ (closed), then $M\equiv N:A$ (definitionally). Which means $Id_A$ internalizes definitional equality.

Fact(1): There is a $P$ such that

But! The type has no proof (not inhabited).

# Function Extensionality / Principle of Extensionality

It is not derivable in **Intentional Type Theory** (ITT). But it is inter-derivable from:

$\eta$:

$\xi$ (weak extensionality):

So it is not derivable in the type theory we developed before, so what do we do about it? There are a few options. One is to justify that there is another form of type theory, so that we can derive the above rule from the new form of type theory.

One is called **Extensional Type Theory** (ETT) or **(Homotopy) Set Theory**.

## Extensional Type Theory (ETT) / (Homotopy) Set Theory

We replace $Id-E$ with the following rules:

reflection:

Note: it is judgemental equlity, not definitional equality.

uniqueness of identity proofs (UIP) / **Discreteness**:

In ETT, Fact(1) means that: $x,y:\mathbb{N}\vdash x+y=y+x:\mathbb{N}$, and so it follows as a corollary that: $\lambda_x\lambda_y.x+y=\lambda_x\lambda_y.y+x:\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$, then we will have a proof $refl:Id_{\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}}(…,…)$

In ETT, if we think of type $A$ as a space, it is *discrete* in the sense that the
only paths of elements of $A$ are the paths between elements and themselves. There is
no path between two different points. We say that as a *Homotopically discrete* space, which
is called a *set*, which is totally different from mathematic’s set theory.

Besides ETT, we can justify another form of type theory, called **Observational Type Theory** (OTT).

## Observational Type Theory

It is another attempt at dealing with the idea that types are homotopically discrete.

Define: by induction on the structure of $A$:

So that the function extensionality can be proof here in OTT