[FOM] formal proofs

[Urs Schreiber]

On 10/23/14, Freek Wiedijk <freek at cs.ru.nl> wrote in small part:

> Also, I would like to understand the models of HoTT better.


That's a good attitude.

One basic fact of homotopy theory is this: The homotopy theory of
topological spaces is equivalent to that of simplicial sets [1] is
equivalent to that of cubical sets [2].

Simplicial sets offer one way to explicit interpret HoTT [3]. Cubical
sets another one [4]. Both have various practical advantages and
disadvantages.

As an entry point for the general issue of models of HoTT I strongly
recommend Michael Shulman's 2012 article [6]

[1] http://ncatlab.org/nlab/show/homotopy+hypothesis
[2] http://ncatlab.org/nlab/show/model+structure+on+cubical+sets#HomotopyTheory
[3] http://ncatlab.org/nlab/show/model+structure+on+simplicial+sets#KapulkinLumnsdaineVoevodsky12
[4] http://ncatlab.org/nlab/show/cubical+set#Cisinski14
[5] http://ncatlab.org/nlab/show/homotopy+type+theory#Shulman12
[6] http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Shulman12