- Family of Types
- “Axiom” (Theorm) of Choice
- Natural Numbers
- Identity Type
- Function Extensionality / Principle of Extensionality
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:Arightarrow 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 $ycdot 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 $Mequiv 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_xlambda_y.x+y=lambda_xlambda_y.y+x:mathbb{N}rightarrowmathbb{N}rightarrowmathbb{N}$,
then we will have a proof $refl:Id_{mathbb{N}rightarrowmathbb{N}rightarrowmathbb{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
近期评论