Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Semantics of QIITs ?
@ 2019-05-16 14:57 Bas Spitters
  2019-05-16 15:39 ` Thorsten Altenkirch
  2019-05-21 11:47 ` [HoTT] " Andrew Swan
  0 siblings, 2 replies; 19+ messages in thread
From: Bas Spitters @ 2019-05-16 14:57 UTC (permalink / raw)
  To: homotopytypetheory

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters
@ 2019-05-16 15:39 ` Thorsten Altenkirch
  2019-05-16 15:50   ` Bas Spitters
  2019-05-21 11:47 ` [HoTT] " Andrew Swan
  1 sibling, 1 reply; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-16 15:39 UTC (permalink / raw)
  To: Bas Spitters, homotopytypetheory; +Cc: Ambrus Kaposi, Kovács András

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/99645C4A-A893-459A-B027-5607E89A37EF%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-16 15:39 ` Thorsten Altenkirch
@ 2019-05-16 15:50   ` Bas Spitters
  2019-05-16 16:15     ` András Kovács
  0 siblings, 1 reply; 19+ messages in thread
From: Bas Spitters @ 2019-05-16 15:50 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: homotopytypetheory, Ambrus Kaposi, Kovács András

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-16 15:50   ` Bas Spitters
@ 2019-05-16 16:15     ` András Kovács
  2019-05-16 18:50       ` Bas Spitters
  0 siblings, 1 reply; 19+ messages in thread
From: András Kovács @ 2019-05-16 16:15 UTC (permalink / raw)
  To: Bas Spitters; +Cc: Thorsten Altenkirch, homotopytypetheory, Ambrus Kaposi

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

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

Bas Spitters <b.a.w.spitters@gmail.com> ezt írta (időpont: 2019. máj. 16.,
Cs, 17:50):

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

-- 
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/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-16 16:15     ` András Kovács
@ 2019-05-16 18:50       ` Bas Spitters
  2019-05-20 16:16         ` Thorsten Altenkirch
  0 siblings, 1 reply; 19+ messages in thread
From: Bas Spitters @ 2019-05-16 18:50 UTC (permalink / raw)
  To: András Kovács
  Cc: Thorsten Altenkirch, homotopytypetheory, Ambrus Kaposi

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

-- 
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/CAOoPQuRVR1A84pFE67GndjCHcUUV_vRCQ8UWdndai%2BzoiqqjZw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-16 18:50       ` Bas Spitters
@ 2019-05-20 16:16         ` Thorsten Altenkirch
  2019-05-20 17:54           ` Bas Spitters
  0 siblings, 1 reply; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-20 16:16 UTC (permalink / raw)
  To: Bas Spitters, András Kovács; +Cc: homotopytypetheory, Ambrus Kaposi

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 16:16         ` Thorsten Altenkirch
@ 2019-05-20 17:54           ` Bas Spitters
  2019-05-20 18:35             ` Thorsten Altenkirch
  0 siblings, 1 reply; 19+ messages in thread
From: Bas Spitters @ 2019-05-20 17:54 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: András Kovács, homotopytypetheory, Ambrus Kaposi

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.

-- 
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/CAOoPQuRJ5QU2GTqctjGSJax0CXkBWWq7GEYcf0EEox3izZTDeQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 17:54           ` Bas Spitters
@ 2019-05-20 18:35             ` Thorsten Altenkirch
  2019-05-20 19:59               ` Jon Sterling
  0 siblings, 1 reply; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-20 18:35 UTC (permalink / raw)
  To: Bas Spitters; +Cc: András Kovács, homotopytypetheory, Ambrus Kaposi

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 18:35             ` Thorsten Altenkirch
@ 2019-05-20 19:59               ` Jon Sterling
  2019-05-20 21:04                 ` Bas Spitters
  0 siblings, 1 reply; 19+ messages in thread
From: Jon Sterling @ 2019-05-20 19:59 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 19:59               ` Jon Sterling
@ 2019-05-20 21:04                 ` Bas Spitters
  2019-05-20 22:17                   ` Thorsten Altenkirch
  0 siblings, 1 reply; 19+ messages in thread
From: Bas Spitters @ 2019-05-20 21:04 UTC (permalink / raw)
  To: Jon Sterling; +Cc: 'Martin Escardo' via Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 21:04                 ` Bas Spitters
@ 2019-05-20 22:17                   ` Thorsten Altenkirch
  2019-05-20 23:26                     ` Jon Sterling
  0 siblings, 1 reply; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-20 22:17 UTC (permalink / raw)
  To: Bas Spitters
  Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

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

> On 20 May 2019, at 22:04, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
> 
> 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.



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/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%40exmail.nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 22:17                   ` Thorsten Altenkirch
@ 2019-05-20 23:26                     ` Jon Sterling
  2019-05-21  0:28                       ` Matt Oliveri
  2019-05-21  8:39                       ` Thorsten Altenkirch
  0 siblings, 2 replies; 19+ messages in thread
From: Jon Sterling @ 2019-05-20 23:26 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

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


On Mon, May 20, 2019, at 6:17 PM, Thorsten Altenkirch wrote:
> 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
> 
> > On 20 May 2019, at 22:04, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
> > 
> > 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.
> 
> 
> 
> 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/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%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/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 23:26                     ` Jon Sterling
@ 2019-05-21  0:28                       ` Matt Oliveri
  2019-05-21  2:45                         ` Jasper Hugunin
  2019-05-21  8:33                         ` Thorsten Altenkirch
  2019-05-21  8:39                       ` Thorsten Altenkirch
  1 sibling, 2 replies; 19+ messages in thread
From: Matt Oliveri @ 2019-05-21  0:28 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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

On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote:
>
> 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
>

-- 
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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-21  0:28                       ` Matt Oliveri
@ 2019-05-21  2:45                         ` Jasper Hugunin
  2019-05-21  8:33                         ` Thorsten Altenkirch
  1 sibling, 0 replies; 19+ messages in thread
From: Jasper Hugunin @ 2019-05-21  2:45 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

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

On Mon, May 20, 2019 at 5:28 PM Matt Oliveri <atmacen@gmail.com> wrote:

> 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.)
>
> On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote:
>>
>> 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
>>
> --
> 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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
> 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/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3YZWAEJAjyLrrbBd71sw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-21  0:28                       ` Matt Oliveri
  2019-05-21  2:45                         ` Jasper Hugunin
@ 2019-05-21  8:33                         ` Thorsten Altenkirch
  2019-05-21 19:56                           ` Matt Oliveri
  1 sibling, 1 reply; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-21  8:33 UTC (permalink / raw)
  To: Matt Oliveri, Homotopy Type Theory


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

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

From: <homotopytypetheory@googlegroups.com> on behalf of Matt Oliveri <atmacen@gmail.com>
Date: Tuesday, 21 May 2019 at 01:28
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Semantics of QIITs ?

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

On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote:
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
--
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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer>.
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/3DC3F379-F057-49AF-9232-CDC925E9646B%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

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

[-- Attachment #2: main.pdf --]
[-- Type: application/pdf, Size: 313696 bytes --]

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-20 23:26                     ` Jon Sterling
  2019-05-21  0:28                       ` Matt Oliveri
@ 2019-05-21  8:39                       ` Thorsten Altenkirch
  1 sibling, 0 replies; 19+ messages in thread
From: Thorsten Altenkirch @ 2019-05-21  8:39 UTC (permalink / raw)
  To: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

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

On 21/05/2019, 00:26, "homotopytypetheory@googlegroups.com on behalf of Jon Sterling" <homotopytypetheory@googlegroups.com on behalf of jon@jonmsterling.com> wrote:

    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
    
    
    On Mon, May 20, 2019, at 6:17 PM, Thorsten Altenkirch wrote:
    > 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
    > 
    > > On 20 May 2019, at 22:04, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
    > > 
    > > 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.
    > 
    > 
    > 
    > 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/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%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/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.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/29D54132-775E-43EE-8439-544FF3EA6C4F%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* [HoTT] Re: Semantics of QIITs ?
  2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters
  2019-05-16 15:39 ` Thorsten Altenkirch
@ 2019-05-21 11:47 ` Andrew Swan
  2019-05-21 12:14   ` Bas Spitters
  1 sibling, 1 reply; 19+ messages in thread
From: Andrew Swan @ 2019-05-21 11:47 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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

On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters 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/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Re: Semantics of QIITs ?
  2019-05-21 11:47 ` [HoTT] " Andrew Swan
@ 2019-05-21 12:14   ` Bas Spitters
  0 siblings, 0 replies; 19+ messages in thread
From: Bas Spitters @ 2019-05-21 12:14 UTC (permalink / raw)
  To: Andrew Swan; +Cc: Homotopy Type Theory

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.

On Tue, May 21, 2019 at 1:47 PM Andrew Swan <wakelin.swan@gmail.com> wrote:
>
> 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
>
> On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters 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/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.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/CAOoPQuTWGc04i%2BcwOFaGLDuD8_b_53hR%3DXRZ7UmHo8-fjO6zOw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 19+ messages in thread

* Re: [HoTT] Semantics of QIITs ?
  2019-05-21  8:33                         ` Thorsten Altenkirch
@ 2019-05-21 19:56                           ` Matt Oliveri
  0 siblings, 0 replies; 19+ messages in thread
From: Matt Oliveri @ 2019-05-21 19:56 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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!

On Tuesday, May 21, 2019 at 4:33:10 AM UTC-4, Thorsten Altenkirch wrote:
>
> 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
>
>  
>
> *From: *<homotopyt...@googlegroups.com <javascript:>> on behalf of Matt 
> Oliveri <atm...@gmail.com <javascript:>>
> *Date: *Tuesday, 21 May 2019 at 01:28
> *To: *Homotopy Type Theory <homotopyt...@googlegroups.com <javascript:>>
> *Subject: *Re: [HoTT] Semantics of QIITs ?
>
>  
>
> 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.)
>
> On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: 
>
> 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
>
>
>

-- 
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/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 19+ messages in thread

end of thread, other threads:[~2019-05-21 19:56 UTC | newest]

Thread overview: 19+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters
2019-05-16 15:39 ` Thorsten Altenkirch
2019-05-16 15:50   ` Bas Spitters
2019-05-16 16:15     ` András Kovács
2019-05-16 18:50       ` Bas Spitters
2019-05-20 16:16         ` Thorsten Altenkirch
2019-05-20 17:54           ` Bas Spitters
2019-05-20 18:35             ` Thorsten Altenkirch
2019-05-20 19:59               ` Jon Sterling
2019-05-20 21:04                 ` Bas Spitters
2019-05-20 22:17                   ` Thorsten Altenkirch
2019-05-20 23:26                     ` Jon Sterling
2019-05-21  0:28                       ` Matt Oliveri
2019-05-21  2:45                         ` Jasper Hugunin
2019-05-21  8:33                         ` Thorsten Altenkirch
2019-05-21 19:56                           ` Matt Oliveri
2019-05-21  8:39                       ` Thorsten Altenkirch
2019-05-21 11:47 ` [HoTT] " Andrew Swan
2019-05-21 12:14   ` Bas Spitters

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).