Free higher groups

[David Wärn]

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

[Ulrik Buchholtz]

Congratulations, that's really great!

And indeed, this is going to be very useful in general: for instance, together with Tom de Jong and Egbert Rijke, we used your work as an input to give a short constructive proof of the non-triviality of the Higman group. I'll talk about this in Vienna on Sunday.

Best wishes,

Ulrik

[Peter LeFanu Lumsdaine]

Lovely — congratulations!  I remember at the IAS special year discussing (with Guillaume Brunerie and others) the feeling that there should be a James construction style proof of Blakers–Massey, but we were never able to find it — fantastic to see that it can be made to work after all.   And the timing is nice — it’s almost exactly 10 years since the final seminar of the special year, where Guillaume, Dan and I presented a survey of the results in synthetic homotopy theory so far, including Blakers–Massey and the James construction:  https://www.ias.edu/video/univalent/1213/0411-HomotopyGroup

Best,

–Peter.

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

[Jon Sterling]

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

[Nicolai Kraus]

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

 

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com.

[Michael Shulman]

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?

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com.

[Dan Christensen]

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

[Michael Shulman]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca.

[Dan Christensen]

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

[Steve Awodey]

good one!
How about just covering a type by a 0-type?

Steve

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo.ca.

[Ulrik Buchholtz]

How about just covering a type by a 0-type?

We have countermodels for this, see: https://ncatlab.org/nlab/show/n-types+cover#InModels

A question that came up for me recently is whether we can construct the modality for which the acyclic maps are the left class. (This exists in every Grothendieck higher topos. In infinity groupoids, and many, but not all, models, the right class are the hypoabelian maps.)

Then there's the question whether every simply connected acyclic type is contractible. (This is open for Grothendieck higher toposes, AFAIK.)

These are mentioned in the talk I mentioned up-thread, which also contained the short new proof that the Higman group presentation is non-trivial and aspherical (as well as acyclic). The slides are here: https://ulrikbuchholtz.dk/hott-uf-2023.pdf

Cheers,

Ulrik

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/21ED9406-6C3A-4B26-A74B-34C2821C97B6%40gmail.com.

[Dan Christensen]

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

[Jasper Hugunin]

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).

[Steve Awodey]

Glad I asked - thanks!

[Michael Shulman]

Bringing this thread back to David's original announcement of his new result, one thing that intrigues me about it is that proceeds by constructing successive approximations to the desired path space and then taking a sequential colimit.  This reminds me of some other sequential constructions that also achieved surprising (to me) things, like Egbert's join construction for building propositional truncation out of nonrecursive HITs, and the splitting of a quasi-idempotent by a sequential (co)limit that Lurie used in higher category theory and I then adapted to HoTT.  I wonder if there are other surprising applications of this principle.

[Thorsten Altenkirch]

One option would be the solution to the coherence problem for Categories with Families (CWFs). Define a wild CWF as a CWF-algebra with no truncation. The question is whether the usual set-truncated initial CWF is weakly initial for wild CWFs. By initial I mean given a set of generating types and terms (otherwise everything is empty). We don’t yet have a construction for this even using 2LTT but we think it should be possible using semi-simplicial types. On the other hand we should be able to encode semi-simplicial types in the initial CWF (ok we may need some Pi-types) and hence the solution to the coherence pro0blem would imply the constructability of semi-simplicial types.

 

Thorsten

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

[Thorsten Altenkirch]

Actually it is sufficient to construct a morphism to tge wild CWF of types.

Sent from Outlook for iOS

---

From: 'Thorsten Altenkirch' via Homotopy Type Theory <HomotopyT...@googlegroups.com>
Sent: Tuesday, May 2, 2023 9:35:55 AM
To: Jasper Hugunin <jas...@hugunin.net>; Homotopy Type Theory <homotopyt...@googlegroups.com>

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.