How Univalence can be used for proofs about algorithm correctness

Question

I read a book on homotopy type theory. HoTT has the univalence axiom. This axiom seems to simplify working in category theory, but which other fields of mathematics it simplifies? I.e. how can I use it, for example, to simplify a proof of correctness of an implementation of red-black trees?

Answer 1

The univalence axiom is not a magic wand that solves all problems.

Univalence has an immense explanatory power because it makes mathematically precise the intuition that "isomorphic structures can be used interchangably". Mathematicians casually use this intuition to pretend that two isomorphic things are actually equal when they are not. Univalence formally justifies the practice.

In the HoTT book you will find many applications of the univalence axiom which simplify or improve the standard approaches, especially in combination with the higher-inductive types.

1. The computation of the fundamental group of the circle.
2. Development of category theory, as you observed.
3. The definition of cardinals is conceptually clean and well-motivated when we use truncation to define them, see chapter 10.
4. Some homotopy-theoretic theorems, such as Blakers-Massey and the Freudentahl suspenion theorem.

Please note that in order to measure "simplification" you have to include the background theory as well. For example, the standard treatment of the fundamental group of the circle includes: construction of real numbers, basic general topology, the topology of euclidean spaces, and the theory of covering spaces.

We do not at the moment have direct applications of the Univalence axiom in theoretical computer science because we do not have a good computational interpretation of univalence. There is the constructive cubical sets model which an important step forward, but some time will probably be needed before applications to specific problems in computer science appear.