<div dir="ltr"><div><div>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.<br>
<br></div>I found something that seems to confirm it. On the nlab page <a href="http://ncatlab.org/nlab/show/type+of+types">type of types</a> 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".<br>
<br></div>Ok, that's a lot of hard words to understand, but then at the linked article <a href="http://ncatlab.org/nlab/show/%28sub%29object+classifier+in+an+%28infinity%2C1%29-topos">(sub)object classifier in an (infinity,1)-topos</a>, 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.<br>
<br>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<br><br>Joe<br></div>