# Univalent Axiom

This is a formalization of the paper "A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom" by Martín Hötzel Escardó, October 18, 2018.
Univalence axiom is not true or false, it is a property of Martin-Löf's identity type of a universe of types.
We can create models of the identity type in these theories, which will make univalence axiom hold or fail.
The idea is that `Id(X, x, y)` collects the ways in which `x` and `y` are identified.
The constructor `refl` identifies any element with itself. Without univalence, `refl` is the only given way to construct elements of the identity type.
The induction over the identity type give rise to a function we call `id_ind` (`J` in the paper).
• Xie: Is it possible to implement `replace` by `id_ind` (or induction of `Id`)?
error
```function replace(
implicit X: Type,
implicit from: X,
implicit to: X,
target: Id(X, from, to),
motive: (X) -> Type,
base: motive(from),
): motive(to) {
return induction (target) {
motive (from, to, target) => motive(to)
case refl => base
// I infer the type to be:
//   motive(from)
// But the expected type is:
//   motive(x)
motive (_from, _to, target) => motive(to)
case refl => base
// I infer the type to be:
//   motive(from)
// But the expected type is:
//   motive(to)
}
}```
Then, in summary, the identity type is given by the data `Id`, `refl`, `id_ind`. With this, the exact nature of the type `Id(X, x, y)` is fairly under-specified. It is consistent that it is always a subsingleton in the sense that `K(X)` holds.
• Subsingleton types: types whose elements are all identified.
The `K` axiom says that `K(X)` holds for every type `X`.
wishful-thinking
```function K_axiom(X: Type): K(X) {
}```
In univalent mathematics, a type `X` that satisfies `K(X)` is called a set.
And with this terminology, the `K` axiom says that all types are sets.
On the other hand, the univalence axiom provides a means of constructing elements of identity type other than `refl`, at least for some types, and hence the univalence axiom implies that some types are not sets.
(Then they will instead be 1-groupoids, or 2-groupoids, ... , or even ∞-groupoids, with such notions defined within MLTT rather than via models, but we will not address this important aspect of univalent mathematics here).
• Xie: In cicada we have type in type.
• Xie: Thus we define a simple universe `U` to be `Type`.
TODO Define `Group` as is in the paper.
With univalence, `Group` itself will not be a set, but a 1-groupoid instead, namely a type whose identity types are all sets. Moreover, if `U` satisfies the univalence axiom, then for `A: Group, B: Group`, the identity type `Id(Group, A, B)` can be shown to be in bijection with the group isomorphisms of `A` and `B`.
Univalence is a property of the identity type `Id(U)` of a universe `U`.
• Xie: We will define univalence axiom for `Id(Type)`?
It takes a number of steps to define the univalence type.
We say that a type `X` is a singleton if we have an element `c: X` with `Id(X, c, x)` for all `x: X`. In Curry-Howard logic, this is
For a function `f: (X) -> Y` and an element `y: Y`, its fiber is the type of points `x: X` that are mapped to (a point identified with) `y`:
The function f is called an equivalence if its fibers are all singletons:
• Xie: Is the following the normal definition of homotopy equivalence?
The type of equivalences from `X: Type` to `Y: Type` is
• Xie: TODO Why homotopy equivalence can be define by singleton and fiber?
Given `x: X`, we have the singleton type consisting of the elements `y: X` identified with `x`:
We also have the element `eta(x)` of this type:
We now need to prove that singleton types are singletons:
Now, for any type `X`, its identity function `id(X)`, defined by `id(x) = x`, is an equivalence. This is because the `Fiber(id, x)` is simply the singleton type defined above, which we proved to be a singleton. We need to name this function:
The identity function `id(X)` should not be confused with the identity type `Id(X)`. Now we use `id_ind` a second time to define a function
Finally, we say that the universe `U` is univalent if the map `id_to_equivalent(X, Y)` is itself an equivalence:
• Xie: `Type` is our only universe.
The type `type_is_univalent` may or may not have an inhabitant. The univalence axiom says that it does. The `K` axiom implies that it doesn't. Because both univalence and the `K` axiom are consistent, it follows that univalence is undecided in MLTT.
TODO