[FOM] Alternative foundations?

[David Roberts]

Hi,

On 22 Feb 2014 09:59, "Hendrik Boom" wrote:

> Subsuming logic into the type theory has been around since
> Martin-Lof's intuitionistic type theory.

Yes, I should have mentioned Martin-Löf's work, and also the computational
side of things, as Henk pointed out.

> ... turns the traditional stack of
> concepts (with sets at the bottom and homotopy one of the specialized
> branches at the top) upside down.

Since the homotopy category is not concrete, one cannot represent homotopy
theory simply via sets with structure, but are forced to consider a
quotient of some category of models, and this is always a large category.
Hence Quillen's work on model categories.

This means a lot of machinery is necessary to treat homotopy theory, not to
mention more exotic variants such as the motivic homotopy theory that went
into eg  Voevodsky's work on the Bloch-Kato conjecture. Homotopy theory is
baked in from the start with homotopy type theory, in that types can be
interpreted as carrying homotopy-theoretic information, and one recovers
sets as the homotopy types with no higher homotopical information
(analogous to how sets can be recovered as the discrete topological
spaces). The program at the IAS, in their book, show how to recover both a
model of the elementary theory of the category of sets, and the von Neumann
cumulative hierarchy.

Cheers,

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140222/0d16d0de/attachment.html>