The Coq mailing list

[Thomas Streicher <streicher AT mathematik.tu-darmstadt.de>]

Dear Vladimir,

in order to formalize the simplicial sets models in type theory I
think one has to use a universe just as you use a Grothendieck universe
(aka strongly inaccessible cardinal) in the set theoretic account.

I think one has to use universes (as in your notes) because otherwise
one would have problems to to ensure the Beck-Chevalley condition
(that substitution commutes logical operations).

Best, Thomas

> my foundations setup is grounded in ZFC through what I call the univalent 
> model of type theory. Formalizing this model is an important and 
> interesting undertaking.  It can be done in a subset of Coq which does  not 
> use universes. This is a whole area of work which has to be done. 
> 
> The way I see it one needs first to formalize the language of coq in a much 
> more simple type theory and then inside this "decidable" type theory to 
> build the required models. 
> 
> A non-formal description of  the univalent model can be found on my website 
> in "Notes on Type Systems".