<p>The univalence axiom is not a magic wand that solves all problems.</p>

<p>Univalence has an immense <em>explanatory</em> 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.</p>

<p>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.</p>

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

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2014-12-29T05:21:55.160Z
This is all true, however people do _hope_ for some specific applications to CS, see e.g. [these slides](http://dlicata.web.wesleyan.edu/pubs/lh122tttalks/lh12wg2.8.pdf) by Dan Licata.
Mike Shulman
CC BY-SA 3.0
2014-12-29T14:03:08.207Z
It's always good to have some hopes.
Andrej Bauer
CC BY-SA 3.0
2014-12-23T20:27:09.730Z
2014-12-23T22:12:10.990Z
2014-12-23T22:12:10.990Z
Andrej Bauer
<p>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?</p>

<type-theory><homotopy-type-theory>
How Univalence can be used for proofs about algorithm correctness
Konstantin Solomatov
# How Univalence can be used for proofs about algorithm correctness

(Asked by: username_0 on 2014-12-23)

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?

**Tags:** type-theory, homotopy-type-theory


---

## 1 answers

### Answer by username_1 on 2014-12-23. Score: 7 | Accepted answer

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.

> **Comments:**
> **username_2**: This is all true, however people do _hope_ for some specific applications to CS, see e.g. [these slides](http://dlicata.web.wesleyan.edu/pubs/lh122tttalks/lh12wg2.8.pdf) by Dan Licata.  
> **username_1**: It's always good to have some hopes.  

---

