Semantics of QIITs ?

[Bas Spitters]

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

[Thorsten Altenkirch]

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

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

[Bas Spitters]

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

[András Kovács]

Hi,

In "Constructing QIITs", we only considered signatures and their semantics in the setting of extensional TT. It is currently an open problem whether construction of QIITs (in the style of our paper) can be performed without UIP, and also whether the syntax of QIIT signatures itself is constructible in such setting. Jasper Hugunin's recent work on constructing some inductive-inductive types in cubical TT could relevant here.

best regards

András

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.com.

[Bas Spitters]

Thanks for confirming that this is still open in homotopical models.

[Thorsten Altenkirch]

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

Thanks for confirming that this is still open in homotopical models.

[Bas Spitters]

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?

> --
> 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/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.nottingham.ac.uk.

[Thorsten Altenkirch]

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

[Jon Sterling]

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

> https://groups.google.com/d/msgid/HomotopyTypeTheory/FBCD91A3-4A6F-456E-93FA-E36EFB56D607%40exmail.nottingham.ac.uk.

[Bas Spitters]

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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.com.

[Thorsten Altenkirch]

What exactly do you mean by “a model”? I’d think we can interpret them in cubical sets using the general construction of HITs. They don’t seem to cause problems in cubical Agda as far as I can see.

Sent from my iPhone

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%40mail.gmail.com.

[Jon Sterling]

Dear Thorsten,

As Andras noted in his message to this thread, it is very much an open question whether QIITs can be modeled without using UIP (this is part of what people are trying to distinguish from, when they are asking about "homotopical" models); therefore, "interpreting them in cubical sets using the general construction of HITs" is definitely not a slam-dunk, and novel + worthwhile research will be needed to determine if it works.

Echoing Andras, I recall that a new encoding due to Jasper Hugunin enable us to interpret IITs without using UIP, and it is an open question to determine whether Jasper's ideas can be extended to QIITs. I hope they can, and someone should find out :)

Best,
Jon

> https://groups.google.com/d/msgid/HomotopyTypeTheory/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%40exmail.nottingham.ac.uk.

[Matt Oliveri]

I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.)

[Jasper Hugunin]

Hello all,

To confirm what others have said about my construction:

As Andras and Jon noted, it remains open whether the construction can be extended to reduce higher inductive-inductive types to higher inductive types, but I am hopeful that it can, at least in a situation such as CTT where the eliminator computes on path constructors.

As Matt noted, the general recursive-recursive eliminator is both essential (for proving initiality, for example) and missing. This is the same restriction as on the construction in extensional type theory (or using UIP) given by Nordvall Forsberg. The main obstacle I see to getting the general recursive-recursive eliminator is that the simple eliminator is not strict, but only computes up to a path. I think I see a way to turn a strict simple eliminator into a general eliminator, but this is still conjectural.

To summarize my understanding of the original question, QIITs are an obvious subset of HIITs, and we know how to handle many HITs primitively in cubical type theory, but the extension to primitive HIITs in cubical type theory has not been done, nor does my construction immediately allow reducing HIITs to HITs (and even if extended lacks strictness and generality of the eliminator).

Best regards,

- Jasper Hugunin

--

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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com.

[Thorsten Altenkirch]

This problem has been solved – see our TYPES 2018 abstract (attached).

 

Basically the idea is to define a relation between “pre-terms” and the semantics and then show that this is contractible for “well-typed objects”, this way you avoid the mutual dependency. This was an idea by Andras Kovacs. In this year’s TYPES there are two abstracts that show how this can be used to give a universal reduction from Inductive-Inductive types to indexed inductive types and hence W-types.

 

I have discussed this with Jesper when he was in Nottingham and I think our tentative conclusion was that this could be combined with his approach to provide a reduction for IITs. However, this needs to be checked.

 

Thorsten

--

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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Thorsten Altenkirch]

Hi Jon,

Thank you for this explanation. Indeed, I think the question of how to interpret QITs without UIP is interesting and open.

I do think the setoid model is useful in this context. It can be defined without using UIP by using propositional relations. Within this model you have limited instances of choice, namely for types that can be obtained by the embedding. Hence I think that QITs that just require countable choice like the Reals should not be a problem. However, this does not give you an explanation for infinitary QITs indexed over a QIT but I don't actually know a natural example of such a thing.

Thorsten

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.com.

[Andrew Swan]

Regarding the Cauchy reals, I believe it is known that countable choice holds and set quotients exist in simplicial sets, but I think under these conditions the usual construction of the Cauchy reals as a quotient of sequences of rationals satisfies the constructors for the HIT Cauchy reals, and also the higher induction principle.

I think the HIT cumulative hierarchy can be constructed using W types and univalence, using the characterisation of it as a retract of the Aczel cumulative hierarchy by Hakon Gylterud in the paper at https://doi.org/10.1017/jsl.2017.84 . If so, similar arguments should work for ordinals and surreal numbers.

Are there any other examples in the HoTT book?

Best,

Andrew

[Bas Spitters]

Thanks. Yes, if we have CAC and set-quotients things simplify.
Of course, the reason to use QIITs is precisely to have a more general
treatment when CAC is not available.

> --
> 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/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com.

[Matt Oliveri]

Thanks. This sounds a lot like the interpreter I did (https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/) that required UIP, and like Streicher's method for proving initiality of the syntax of dependent type theory. Combining it with Hugunin's technique sounds promising!