[HoTT-reading-group] space of spaces

[Bas Spitters]

Very quick answer: there is a section on the object classifier in the book.
This may help filling in the details.

On Tue, Feb 4, 2014 at 8:04 AM, Joe Hannon <hannon at math.bu.edu> wrote:
> 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
> 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, 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
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>