[HoTT] Free higher groups

[HoTT] Free higher groups

[David Wärn]

[-- Attachment #1: Type: text/plain, Size: 817 bytes --]

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-77db-5cbf56da17f3%40gmail.com.

[-- Attachment #2: po-paths.pdf --]
[-- Type: application/pdf, Size: 314831 bytes --]

[HoTT] Re: Free higher groups

[Ulrik Buchholtz]

[-- Attachment #1.1: Type: text/plain, Size: 1281 bytes --]

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


On Friday, April 21, 2023 at 12:04:20 PM UTC+2 cod...@gmail.com 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/4e1cf0e3-a5b0-4014-b144-0a5bb98b01e3n%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 1872 bytes --]

Re: [HoTT] Free higher groups

[Peter LeFanu Lumsdaine]

[-- Attachment #1: Type: text/plain, Size: 2014 bytes --]

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.






On Fri, Apr 21, 2023 at 11:04 AM David Wärn <codwarn@gmail.com> 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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-kzRC70p5Xpv8YANJqUgHbDMj2y5e6A2x4RX8WbAEseag%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 3084 bytes --]

Re: [HoTT] Free higher groups

[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


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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com.

Re: [HoTT] Free higher groups

[Nicolai Kraus]

[-- Attachment #1: Type: text/plain, Size: 2527 bytes --]

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 <jon@jonmsterling.com> 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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 3731 bytes --]

Re: [HoTT] Free higher groups

[Michael Shulman]

[-- Attachment #1: Type: text/plain, Size: 3792 bytes --]

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 <nicolai.kraus@gmail.com>
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 <jon@jonmsterling.com> 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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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/CADYavpxM-_a_nM0qu7XBv66oP8VG852BaMwmzo3%2BNgGxijf8Rg%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 5395 bytes --]

Re: [HoTT] Free higher groups

[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

On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> 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
> <nicolai.kraus@gmail.com> 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
>     <jon@jonmsterling.com> 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
>         HomotopyTypeTheory+unsubscribe@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
>         HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca.

Re: [HoTT] Free higher groups

[Michael Shulman]

[-- Attachment #1: Type: text/plain, Size: 5943 bytes --]

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 <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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
> > <nicolai.kraus@gmail.com> 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
> >     <jon@jonmsterling.com> 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
> >         HomotopyTypeTheory+unsubscribe@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
> >         HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxy1Qh97%2BPZ1%3DDaaKFH3RXo9wTwDhqbcoUFw5ZDP4oUrQ%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 8522 bytes --]

Re: [HoTT] Free higher groups

[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

On Apr 28, 2023, Michael Shulman <shulman@sandiego.edu> 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 <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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
>  > <nicolai.kraus@gmail.com> 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
>  >     <jon@jonmsterling.com> 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
>  >         HomotopyTypeTheory+unsubscribe@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
>  >         HomotopyTypeTheory+unsubscribe@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
>  HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo.ca.

Re: [HoTT] Free higher groups

[Steve Awodey]

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

Steve


> On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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 <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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
>>> <nicolai.kraus@gmail.com> 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
>>>    <jon@jonmsterling.com> 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
>>>        HomotopyTypeTheory+unsubscribe@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
>>>        HomotopyTypeTheory+unsubscribe@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
>> HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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/21ED9406-6C3A-4B26-A74B-34C2821C97B6%40gmail.com.

Re: [HoTT] Free higher groups

[Ulrik Buchholtz]

[-- Attachment #1: Type: text/plain, Size: 8148 bytes --]

> 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


> Steve
>
>
> > On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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 <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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
> >>> <nicolai.kraus@gmail.com> 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
> >>>    <jon@jonmsterling.com> 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
> >>>        HomotopyTypeTheory+unsubscribe@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
> >>>        HomotopyTypeTheory+unsubscribe@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
> >> HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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/21ED9406-6C3A-4B26-A74B-34C2821C97B6%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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAE-BQ1zWQHqUv9woQPw75Sqz1c7_M9F-nzX3RYYmXAxVxy8skQ%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 12423 bytes --]

Re: [HoTT] Free higher groups

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 8900 bytes --]

Glad I asked - thanks!

> On Apr 29, 2023, at 2:49 PM, Ulrik Buchholtz <ulrikbuchholtz@gmail.com> wrote:
> 
>> 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
> 
>> 
>> Steve
>> 
>> 
>> > On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca <mailto:jdc@uwo.ca>> 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 <shulman@sandiego.edu <mailto:shulman@sandiego.edu>> 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 <jdc@uwo.ca <mailto:jdc@uwo.ca>> 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 <shulman@sandiego.edu <mailto:shulman@sandiego.edu>> 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
>> >>> <nicolai.kraus@gmail.com <mailto:nicolai.kraus@gmail.com>> 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
>> >>>    <jon@jonmsterling.com <mailto:jon@jonmsterling.com>> 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
>> >>>        HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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
>> >>>        HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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
>> >> HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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 <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/21ED9406-6C3A-4B26-A74B-34C2821C97B6%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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/5D0912E6-075B-47EE-87B8-8B5118DDF07C%40gmail.com.

[-- Attachment #2: Type: text/html, Size: 13229 bytes --]

Re: [HoTT] Free higher groups

[Michael Shulman]

[-- Attachment #1: Type: text/plain, Size: 1049 bytes --]

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.

-- 
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/CADYavpzinvAW_PgLUPbp4NyykJxhEbmBsQSC6rQroZWCcFg9xw%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 1375 bytes --]

Re: [HoTT] Free higher groups

[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

On Apr 29, 2023, Steve Awodey <steveawodey@gmail.com> wrote:

> good one!
> How about just covering a type by a 0-type?
>
> Steve
>
>> On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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 <jdc@uwo.ca> 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 <shulman@sandiego.edu> 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
>>>> <nicolai.kraus@gmail.com> 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
>>>>    <jon@jonmsterling.com> 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
>>>>        HomotopyTypeTheory+unsubscribe@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
>>>>        HomotopyTypeTheory+unsubscribe@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
>>> HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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/87r0s2y0rp.fsf%40uwo.ca.

Re: [HoTT] Free higher groups

[Jasper Hugunin]

[-- Attachment #1.1: Type: text/plain, Size: 7687 bytes --]

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 
<http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>).

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 <steve...@gmail.com> wrote:
>
> > good one!
> > How about just covering a type by a 0-type?
> >
> > Steve
> >
> >> On Apr 29, 2023, at 1:37 PM, Dan Christensen <j...@uwo.ca> 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 <shu...@sandiego.edu> 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 <j...@uwo.ca> 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 <shu...@sandiego.edu> 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
> >>>> <nicola...@gmail.com> 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
> >>>> <j...@jonmsterling.com> 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.

[-- Attachment #1.2: Type: text/html, Size: 13646 bytes --]

Re: [HoTT] Free higher groups

['Thorsten Altenkirch' via Homotopy Type Theory]

[-- Attachment #1: Type: text/plain, Size: 9324 bytes --]

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

From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of Jasper Hugunin <jasper@hugunin.net>
Date: Saturday, 29 April 2023 at 20:08
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Free higher groups
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<http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>).

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 <steve...@gmail.com> wrote:

> good one!
> How about just covering a type by a 0-type?
>
> Steve
>
>> On Apr 29, 2023, at 1:37 PM, Dan Christensen <j...@uwo.ca> 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 <shu...@sandiego.edu> 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 <j...@uwo.ca> 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 <shu...@sandiego.edu> 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
>>>> <nicola...@gmail.com> 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
>>>> <j...@jonmsterling.com> 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<mailto: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<https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com?utm_medium=email&utm_source=footer>.



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.




-- 
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/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.

[-- Attachment #2: Type: text/html, Size: 16361 bytes --]

Re: [HoTT] Free higher groups

['Thorsten Altenkirch' via Homotopy Type Theory]

[-- Attachment #1: Type: text/plain, Size: 10901 bytes --]

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

Sent from Outlook for iOS<https://aka.ms/o0ukef>
________________________________
From: 'Thorsten Altenkirch' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Sent: Tuesday, May 2, 2023 9:35:55 AM
To: Jasper Hugunin <jasper@hugunin.net>; Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Free higher groups


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



From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of Jasper Hugunin <jasper@hugunin.net>
Date: Saturday, 29 April 2023 at 20:08
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Free higher groups

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<http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>).



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 <steve...@gmail.com> wrote:

> good one!
> How about just covering a type by a 0-type?
>
> Steve
>
>> On Apr 29, 2023, at 1:37 PM, Dan Christensen <j...@uwo.ca> 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 <shu...@sandiego.edu> 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 <j...@uwo.ca> 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 <shu...@sandiego.edu> 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
>>>> <nicola...@gmail.com> 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
>>>> <j...@jonmsterling.com> 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<mailto: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<https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com?utm_medium=email&utm_source=footer>.



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.





--
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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>.



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.




-- 
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/PAXPR06MB78695C1CF6057EC48042EC03CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.

[-- Attachment #2: Type: text/html, Size: 17665 bytes --]