What is the relation between (and status of) the Univalent Foundations and Homotopy Type Theory?

Question

It appears as though UniMath and HoTT on GitHub are both active up til and including today. The Wikipedia pages have both linking to each other.

Without being steeped in both areas, how do they relate, and what is the status of the two projects? Does HoTT supercede UniMath, such that UniMath is a legacy/prior incarnation of the general foundations, and HoTT is the newest latest development of the idea/thread? Or are they competing in some way?

Answer 1

First, let me note that the title of this question is misleading: the difference between Univalent Foundations and Homotopy type theory is a separate question from the difference between UniMath and the HoTT library. (The former are described well by their Wikipedia articles, so the reader interested in that question may be referred there.)

UniMath and the HoTT library are both libraries for mathematics according to a univalent principle, in the language of (variations of) homotopy type theory. Though UniMath originated first, growing out of Voevodsky's Foundations library, both are still in active development. The introduction to Bauer–Gross–Lumsdaine's The HoTT Library: A formalization of homotopy type theory in Coq explains the difference in philosophy between the two projects (under the section Consistency).

The essential difference is that UniMath takes the stance of distrusting Coq as much as possible, using only the most basic language features (e.g. these present in Martin-Löf Type Theory), because Coq's type system is, in places, ad hoc, and it has not been demonstrated these combinations of features are actually sound. By avoiding advanced (unproven) language features, UniMath hopes to avoid possible inconsistency arising from an unsound type system.

On the other hand, the HoTT library is concerned more with formalisation that is more user-friendly, thus permitting advanced language features, at the cost of potentially introducing unsoundness when using unproven features of Coq:

For this reason [avoiding potential inconsistency], UniMath avoids almost all of Coq’s features (even e.g. record types), restricting itself as far as possible to standard Martin-Löf type theory (except for assuming Type : Type throughout, to simulate Voevodsky’s resizing rules). However, this restriction cannot be enforced by the kernel. We feel rather that proof assistants and computerized formalization of mathematics are at such an early stage that it is well worth experimenting, even at the risk of introducing an inconsistency (which is fairly slight, due to the known semantic accounts of fragments of the theory).

Pragmatically, since the libraries have been developed in parallel, there are also differences in what features the two libraries currently support (such as the range of mathematical definitions and theorems).