Another example constructible in HTS but maybe not in HoTT is the large type of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus ). This one might be a bit tricky because I don't know how to internally express that a particular large type is the type of semi-simplicial types either (what universal property it should have). On Saturday, April 29, 2023 at 11:57:36 AM UTC-7 Dan Christensen wrote: > Sets don't cover in a general oo-topos. (You have to be a bit > careful about the internal notion vs the external notion, but > both fail in general.) There's a good summary here: > > https://ncatlab.org/nlab/show/n-types+cover/ > > Dan > > On Apr 29, 2023, Steve Awodey wrote: > > > good one! > > How about just covering a type by a 0-type? > > > > Steve > > > >> On Apr 29, 2023, at 1:37 PM, Dan Christensen wrote: > >> > >> Another set-level statement is whether there are enough injective > >> abelian groups. It's true in Grothendieck oo-toposes, but presumably is > >> not provable in HoTT. > >> > >> Dan > >> > >> On Apr 28, 2023, Michael Shulman wrote: > >> > >>> The existence of hypercompletion is a good suggestion. > >>> > >>> Also I realized there are set-level statements that are already known > to be > >>> true in all Grothendieck 1-toposes but not all elementary 1-toposes, > such as > >>> WISC and Freyd's theorem that a small complete category is a preorder. > So > >>> those will be true in any Grothendieck oo-topos too, and can be > presumed to > >>> fail in HoTT. But it's nice to have one that involves higher types too. > >>> > >>> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen wrote: > >>> > >>> A not-so-interesting answer to Mike's question is the type of > deloopings > >>> of S^3. The reason this isn't so interesting is that it's in the image > >>> of the natural functor from Spaces to any oo-topos, so it's true just > >>> because it is true for Spaces. Similarly, a statement asserting that > >>> pi_42(S^17) = (insert what it is) is true in any oo-topos. Another > >>> reason these aren't interesting is that I expect that they are provable > >>> in HoTT with enough work. > >>> > >>> So, I'll second Mike's question, with the extra condition that it would > >>> be good to have a type for which there is some reason to doubt that it > >>> is provably inhabited in HoTT. > >>> > >>> Oh, what about whether the hypercomplete objects are the modal > >>> objects > >>> for a modality? I'm throwing this out there without much thought... > >>> > >>> Dan > >>> > >>> On Apr 24, 2023, Michael Shulman wrote: > >>> > >>>> This is fantastic, especially the simplicity of the construction. As > >>>> Peter said, a wonderful way to commemorate the 10th anniversary of > >>> the > >>>> special year and the release of the HoTT Book. > >>>> > >>>> Relatedly to Nicolai's question, this question also has an easy proof > >>>> in any Grothendieck infinity-topos. Now that we know it also has a > >>>> proof in HoTT, do we know of any type in HoTT whose interpretation in > >>>> any Grothendieck infinity-topos is known to be inhabited, but which > >>>> isn't known to be inhabited in HoTT? > >>>> > >>>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > >>>> wrote: > >>>> > >>>> Hi David, > >>>> > >>>> Congratulations (again)! I find it very interesting that this > >>>> question has a positive answer. I had suspected that it might > >>>> separate HoTT from Voevodsky's HTS (aka 2LTT with a fibrancy > >>>> assumption on strict Nat). Since this isn't the case, do we know > >>>> of another type in HoTT that is inhabited in HTS, while we don't > >>>> know whether we can construct an inhabitant in HoTT? > >>>> > >>>> Best, > >>>> Nicolai > >>>> > >>>> On Fri, Apr 21, 2023 at 8:30 PM Jon Sterling > >>>> wrote: > >>>> > >>>> Dear David, > >>>> > >>>> Congratulations on your beautiful result; I'm looking forward > >>>> to understanding the details. Recently I had been wondering if > >>>> anyone had proved this, and I am delighted to see that it is > >>>> now done. > >>>> > >>>> Best wishes, > >>>> Jon > >>>> > >>>> On 21 Apr 2023, at 12:04, David Wärn wrote: > >>>> > >>>>> Dear all, > >>>>> > >>>>> I'm happy to announce a solution to one of the oldest open > >>>> problems in synthetic homotopy theory: the free higher group > >>>> on a set is a set. > >>>>> > >>>>> The proof proceeds by describing path types of pushouts as > >>>> sequential colimits of pushouts, much like the James > >>>> construction. This description should be useful also in many > >>>> other applications. For example it gives a straightforward > >>>> proof of Blakers-Massey. > >>>>> > >>>>> Best wishes, > >>>>> David > >>>>> > >>>>> -- > >>>>> You received this message because you are subscribed to the > >>>> Google Groups "Homotopy Type Theory" group. > >>>>> To unsubscribe from this group and stop receiving emails > >>>> from it, send an email to > >>>> HomotopyTypeThe...@googlegroups.com. > >>>>> To view this discussion on the web visit > >>>> > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-77db-5cbf56da17f3%40gmail.com > . > >>> > >>>> > >>>> -- > >>>> You received this message because you are subscribed to the > >>>> Google Groups "Homotopy Type Theory" group. > >>>> To unsubscribe from this group and stop receiving emails from > >>>> it, send an email to > >>>> HomotopyTypeThe...@googlegroups.com. > >>>> To view this discussion on the web visit > >>>> > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com > . > >>> > >>>> > >>>> -- > >>>> You received this message because you are subscribed to the > >>> Google > >>>> Groups "Homotopy Type Theory" group. > >>>> To unsubscribe from this group and stop receiving emails from it, > >>>> send an email to > >>> HomotopyTypeThe...@googlegroups.com. > >>>> To view this discussion on the web visit > >>>> > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com > . > >>> > >>> -- > >>> You received this message because you are subscribed to the Google > >>> Groups "Homotopy Type Theory" group. > >>> To unsubscribe from this group and stop receiving emails from it, send > >>> an email to HomotopyTypeThe...@googlegroups.com. > >>> To view this discussion on the web visit > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca > . > >> > >> -- > >> You received this message because you are subscribed to the Google > >> Groups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, > >> send an email to HomotopyTypeThe...@googlegroups.com. > >> To view this discussion on the web visit > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo.ca > . -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com.