[FOM] An example in homotopy type theory

[Kevin Watkins]

The subject of homotopy type theory has been mentioned in some recent
posts.  My understanding is that the key feature of this language is the
"univalence axiom".  I thought I might try to give an example of how one
might use the univalence axiom.

I am not an expert in homotopy type theory.  If what I say is imprecise,
hopefully I will be corrected by someone who knows better.

Suppose we would like to define the integers with the operations plus,
negate, and zero on them.

One way is to let Z = N + N, the disjoint union of two copies of the
natural numbers, and define the operations by case analysis in the evident
way.

Another way is to let Z' = N * N / R for a certain equivalence relation R.

We have thereby specified 4-tuples (Z, plus, negate, zero) and (Z', plus',
negate', zero') corresponding to the two different definitions.

In set theory there is no reason to expect these 4-tuples to be equal.

In homotopy type theory it is a theorem that they are equal terms of the
appropriate type.  They are indiscernible in the sense that one can be
substituted for the other in any context varying over that type.  In
particular, if any predicate over that type is true of one, it will be true
of the other.

If this sounds too good to be true, you can download the software and try
it for yourself.  There is a prototype implementation of the language, by
Thierry Coquand and collaborators, at https://github.com/simhu/cubical.

Kevin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140220/109bae83/attachment.html>