The Coq mailing list

[Carlos Simpson <Carlos.Simpson AT unice.fr>]

Dear Vladimir, Thomas,
  I'm not completely sure to have had a well-formulated question, but I think
it was something like the following: is there some kind of sub-collection
of types which are supposed to correspond, semantically, to usual
sets rather than some kind of homotopy types? In a simplicial set model,
this would mean the 0-truncated simplicial sets i.e. those whose higher
homotopy groups vanish. And are they allowed to be ``very big'' in the
sense, say, that there would exist a 0-truncated set 
containing a Grothendieck universe or two? (or more precisely, that such
an axiom would be consistent with the rest of the axiomatic framework)?
  Actually, this question was suggested by your message on the addition to
your library, namely it looked from afar that your new library addition was
destined to say exactly this, is that (approximately) correct? 
  Thomas's message was on the other side of the question, i.e. about how
to realize into an exterior ZFC kind of system; I was asking about the 
possibility of including an ``interior'' ZFC (which of course would probably
need many axioms). 
  Thanks!
---Carlos






Selon 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". 
>