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)?
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.
function K_axiom(X: Type): K(X) {
  return TODO
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.