--
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.
For more options, visit https://groups.google.com/d/optout.
On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote:If we are only interested in providing one -particular- model of HITs, the paperon cubical type theory describes a way to interpret HIT together with a univalentuniverse which is stable by HIT operations. This gives in particular the consistencyand the proof theoretic power of this extension of type theory.
> >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optout.
> >>
> >>
> >>
> >> --
> >> 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+unsub...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optout.
> >>
> >>
> >> --
> >> 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+unsub...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optout.
> >
> > --
> > 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+unsub...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> 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+unsub...@googlegroups.com.
>>> > >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>>> > >> For more options, visit https://groups.google.com/d/optout.
>>> > >>
>>> > >>
>>> > >>
>>> > >> --
>>> > >> 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+unsub...@googlegroups.com.
>>> > >> For more options, visit https://groups.google.com/d/optout.
>>> > >>
>>> > >>
>>> > >> --
>>> > >> 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+unsub...@googlegroups.com.
>>> > >> For more options, visit https://groups.google.com/d/optout.
>>> > >
>>> > > --
>>> > > 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+unsub...@googlegroups.com.
>>> > > For more options, visit https://groups.google.com/d/optout.
>>> >
>>> > --
>>> > 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+unsub...@googlegroups.com.
>>> > For more options, visit https://groups.google.com/d/optout.
>
> --
> 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+unsub...@googlegroups.com.
>> >>> > >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >>
>> >>> > >>
>> >>> > >>
>> >>> > >> --
>> >>> > >> You received this message because you are subscribed to the
>> >>> > >> Groups
>> >>> > >> "Homotopy Type Theory" group.
>> >>> > >> To unsubscribe from this group and stop receiving emails from it,
>> >>> > >> send an
>> >>> > >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >>
>> >>> > >>
>> >>> > >> --
>> >>> > >> You received this message because you are subscribed to the
>> >>> > >> Groups
>> >>> > >> "Homotopy Type Theory" group.
>> >>> > >> To unsubscribe from this group and stop receiving emails from it,
>> >>> > >> send an
>> >>> > >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >
>> >>> > > --
>> >>> > > 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+unsub...@googlegroups.com.
>> >>> > > For more options, visit https://groups.google.com/d/optout.
>> >>> >
>> >>> > --
>> >>> > 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+unsub...@googlegroups.com.
>> >>> > For more options, visit https://groups.google.com/d/optout.
>> >
>> > --
>> > 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+unsub...@googlegroups.com.
>> > For more options, visit https://groups.google.com/d/optout.
>
> --
> 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+unsub...@googlegroups.com.
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
> you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?
Exactly, yes. There’s no reason I know of to think they *need* to, but with the construction of Mike’s and my paper, they do. And adding stronger conditions on the cardinal used won’t help. The problem is that one takes a fibrant replacement to go from the “pre-suspension” to the suspension (more precisely: a (TC,F) factorisation, to go from the universal family of pre-suspensions to the universal family of suspensions); and fibrant replacement blows up the fibers to be the size of the *base* of the family. So the pre-suspension is small, but the suspension — although essentially small — ends up as large as the universe one’s using.
On 7 Jun 2017, at 11:40, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
> you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?
Exactly, yes. There’s no reason I know of to think they *need* to, but with the construction of Mike’s and my paper, they do. And adding stronger conditions on the cardinal used won’t help. The problem is that one takes a fibrant replacement to go from the “pre-suspension” to the suspension (more precisely: a (TC,F) factorisation, to go from the universal family of pre-suspensions to the universal family of suspensions); and fibrant replacement blows up the fibers to be the size of the *base* of the family. So the pre-suspension is small, but the suspension — although essentially small — ends up as large as the universe one’s using.
I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.)
So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.)
So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.)
Why is there no LOG in this?
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.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.