[HoTT-reading-group] space of spaces

[Joe Hannon]

I was looking around on nLab to see if I could get some confirmation for
our decision today that the homotopy theoretic analogue of the type of
types (a so-called space of spaces), should just be the core (subcategory
of isomorphisms) of the category of space.

I found something that seems to confirm it. On the nlab page type of
types<http://ncatlab.org/nlab/show/type+of+types>it says "in homotopy
type theory the type of types Type is often assumed to
satisfy the univalence axiom. This is a reflection of the fact that in its
categorical semantics as an object classifier is part of an internal
(infinity,1)-category in the ambient (infinity,1)-topos".

Ok, that's a lot of hard words to understand, but then at the linked
article (sub)object classifier in an
(infinity,1)-topos<http://ncatlab.org/nlab/show/%28sub%29object+classifier+in+an+%28infinity%2C1%29-topos>,
it says under the section on examples "Proposition 2. The \kappa-compact
object classifier in ∞Grpd is Type κ:=Core(∞Grpd κ)," So modulo size
issues, the subobject classifier which is apparently the right notion of a
"type of types" is just the core of the category of infinity-groupoids,
exactly as we wanted.

But I couldn't understand all the development to get to that statement, so
if someone else understands it better, I'd be interested to hear more

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140204/f942be96/attachment.htm