natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
There are two different fundamental theorems of identity types, depending on whether identity types are defined with plain identity induction or with based identity induction.
The fundamental theorem of identity types states that given a type $A$, a type family $x:A, y:A \vdash B(x, y)$ and a family of functions
the following conditions are equivalent:
For each $x:A$ the dependent sum type of the type family $y:A \vdash B(x, y)$ is a contractible type.
There is a family of equivalences
$B(x, y)$ is an identity system.
For each $x:A$ and $y:A$, the function $f(x, y)$ is an equivalence of types
$f(x, y)$ is a retraction
$R(x, y)$ with the function $f(x, y)$ satisfies the universal property of the unary sum of $x =_A y$.
The fundamental theorem of identity types states that given a type $A$, an element $a:A$, a type family $x:A \vdash B(x)$ and a family of functions
the following conditions are equivalent:
The dependent sum type of the type family $x:A \vdash B(x)$ is a contractible type.
There is a family of equivalences
$B(x)$ equipped with $f(\mathrm{refl}_A(a)):B(a)$ is an identity system.
For each $x:A$, the function $f(x)$ is an equivalence of types
For each $x:A$, $f(x)$ is a retraction
For each $x:A$, $B(x)$ with the function $f(x)$ satisfies the universal property of the unary sum of $a =_A x$.
Suppose the equivalence type used in the second definition is a weak equivalence type. It is possible to show that definitions 1 and 2 are the same.
Definition 1 implies definition 2, because both $\sum_{x:A} (a =_A x)$ and $\sum_{x:A} B(x)$ are contractible types, there is a weak equivalences of types
Given any two families $x:A vdash B(x)$ and $x:A \vdash C(x)$, there is an weak equivalence of types
Thus, there is a family of weak equivalences of types
and we define $\mathrm{ftid}'(x) \coloneqq \mathrm{tot}(f(x))(y)$.
Definition 2 implies definition 1, as we begin with a family of weak equivalences
or equivalently
We can get a weak equivalences
by defining
The type $\sum_{x:A} (a =_A x)$ is always contractible; this means the type $\sum_{x:A} B(x)$ is contractible as well, since the two types are equivalent to each other. Thus, one could construct a witnesses
Suppose the equivalence type used in the second definition is a weak equivalence type. Then definitions 2 and 3 are the same because given any type $A$ and $B$, there is a equivalence
Thus, in one direction, we define
and in the other direction, we inductively define $\mathrm{ftid}'(x)$ by induction on reflexivity
Suppose that for every $x:A$ we have a witness that the function $f(x)$ is an equivalence of types
For every type $A$ and $B$, there is a family of functions
which takes a witness that $f$ is an equivalence to a quasi-inverse function of $f$. The retraction of $f(x)$ is represented by
This proof is adapted from Dan Licata in Licata 16:
Suppose that for every $x:A$ we have a function
and a family of homotopies
This exhibits $B(x)$ as a retract of $a =_A x$, hence $\sum_{x:A} B(x)$ as a retract of the contractible type $\sum_{x:A} a =_A x$, so there is an element
The fundamental theorem of identity types appears in section 11.2 of
Definition 5 arises as a generalization of this proof by Dan Licata for univalent universes:
Last revised on March 6, 2023 at 09:18:26. See the history of this page for a list of all contributions to it.