Re: [HoTT] Semantics of QIITs ?

[Bas Spitters <b.a.w.spitters@gmail.com>]

Do we even have a model that would capture all the QIIT constructions
in the HoTT book?

I recall an argument where one constructs the Cauchy numbers as a QIIT
*within* the Dedekind numbers (assuming impredicativity) and then show
that this indeed has the right initiality property. However, I don't
recall whether anyone ever worked out the details of this, or how
general this method is.

On Mon, May 20, 2019 at 9:59 PM Jon Sterling <jon@jonmsterling.com> wrote:
>
> Hi Thorsten,
>
> I think that in the way I interpreted Bas's question, setoids probably don't count --- by that token, even sets would also be "homotopical" because sets are a special case of setoids which are a special case of groupoids which are a special case of infinity groupoids, but what people are wondering is probably more along the lines of whether there is a model of type theory in which the universes are both univalent and closed under general QIITs. And as Bas notes, non-finitary QIITs are not just a special case of something well-known like generalized algebraic theories or something like that, so there are some really deep questions involved.
>
> This is not a bad thing: it means there are some very interesting questions left to figure out, maybe suitable for an ambitious phd student :)
>
> Best,
> Jon
>
>
>
>
> On Mon, May 20, 2019, at 2:36 PM, Thorsten Altenkirch wrote:
> > The setoid model is just a restriction of the groupoid model where all
> > the Homs are propositional - does this not count as homotopical?
> >
> >
> >
> > Sent from my iPhone
> >
> > > On 20 May 2019, at 18:55, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
> > >
> > > As you say, Mike and Peter note that:
> > > "the idea is that higher inductive types can be used to construct free
> > > algebras for infinitary algebraic theories. However, Blass showed
> > > (modulo a large
> > > cardinal assumption) that these cannot be constructed in ZF [Bla83]."
> > > In fact, they construct an uncountable regular cardinal explicitly (Thm 9.1).
> > > https://arxiv.org/abs/1705.07088
> > > So, QITs do add extra expresivity.
> > >
> > >
> > > My question is about "small" QIITs (Cauchy reals, ...) in homotopical
> > > models, so the setoid model does not really count.
> > > However, has it been proved even in that case that such QIITs exist?
> > >
> > > On Mon, May 20, 2019 at 6:17 PM Thorsten Altenkirch
> > > <Thorsten.Altenkirch@nottingham.ac.uk> wrote:
> > >>
> > >> Do we know wether the existence of QI(I)Ts isn't a new constructive principle?
> > >>
> > >> Mike and Peter show that there are QITs which aren't constructible from quotients. However, we may still be able to justify a type theory with QITs without using them. E.g. in the Setoid model we can construct many QITs including the Reals (I think) but this is maybe because choice is provable for the setoids which are obtained from sets (like Nat). But what about a QIT which uses a setoid for which we don't have choice?
> > >>
> > >> Thorsten
> > >>
> > >>
> > >> On 16/05/2019, 19:50, "Bas Spitters" <b.a.w.spitters@gmail.com> wrote:
> > >>
> > >>    Thanks for confirming that this is still open in homotopical models.
> > >>
> > >>
> > >>
> > >>
> > >>
> > >> 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/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.nottingham.ac.uk.
> > >> For more options, visit https://groups.google.com/d/optout.
> >
> >
> >
> > 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/FBCD91A3-4A6F-456E-93FA-E36EFB56D607%40exmail.nottingham.ac.uk.
> > 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+unsubscribe@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.