Hi Thorsten,

Yes, I saw your result (congratulations!) However, I may be
overlooking something, but do we know that the theory of codes is
available in any of the standard models of HoTT?
That doesn't seem to be stated in your paper.

Best regards,

Bas


On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
> Hi Bas,
>
> Our POPL 2019 paper does address this I think, maybe not exactly in the way you expect. We define a theory of codes (based on earlier work by Ambrus and Andras) which is an intrinsic type theory such that a context is a representation of a quotient inductive-inductive type. The formation of Pi-types is restricted so that you can only form strictly positive types, it is indeed a special case of a directed type theory. Now the semantics are categories with an initial object and it turns out we can construct the semantics just from assuming the existence of the theory of codes. The category assigned to a context is the category of algebras and the initial object is the intended interpretation of the QIIT, equivalently we get the expected elimination principle. The theory of codes can "eat itself" it is an instance of a QIIT definable in itself. Hence this QIIT is in a certain sense universal.
>
> One would also like to interpret QIITs that are indexed by "external" types which are already defined and in particular include infinitary constructors. One can extend the theory but the semantics suffered from a coherence issue. However, I think Andras made some progress on this.
>
> My view is that this programme can be extended to HIITs by considering higher order versions of type theory and in particular the theory of codes. However, this is maybe an overkill, since one can normalize the substitutions (make them implicit) and address the coherence issues this way. I think that is basically what Andras has done.
>
> Here is a link to the pdf:
> https://akaposi.github.io/finitaryqiit.pdf
>
> Thorsten
>
> On 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on behalf of Bas Spitters" <homotopytypetheory@googlegroups.com on behalf of b.a.w.spitters@gmail.com> wrote:
>
>     What is the status of the semantics of quotient inductive inductive types?
>     Looking at the literature there's some progress on reducing QIITs to
>     simpler constructions, but this does not seem to have led to a
>     convenient semantic result.
>     E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman.
>
>     https://ncatlab.org/nlab/show/inductive-inductive+type
>
>     Do we know that the prototypical QIITs from the book (e.g. Cauchy
>     reals) are supported in the usual models of HoTT?
>
>     Thanks,
>
>     Bas
>
>     --
>     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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com.
>     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/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.