Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] HITs in Agda
@ 2019-01-10 13:37 Ali Caglayan
  2019-01-10 13:53 ` [HoTT] " Martín Hötzel Escardó
  2019-01-10 20:53 ` Martín Hötzel Escardó
  0 siblings, 2 replies; 10+ messages in thread
From: Ali Caglayan @ 2019-01-10 13:37 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I just noticed that [agda supposedly has support for 
HITs](https://github.com/agda/agda/issues/2761) since November. Since I 
didn't realise this was the case I am letting people here know too.

Now my questions:

Are these really HITs? 

Do they work without axiom K? 

What can and can't be done with them?

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

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

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

* [HoTT] Re: HITs in Agda
  2019-01-10 13:37 [HoTT] HITs in Agda Ali Caglayan
@ 2019-01-10 13:53 ` Martín Hötzel Escardó
  2019-01-10 15:19   ` Ali Caglayan
  2019-01-10 20:53 ` Martín Hötzel Escardó
  1 sibling, 1 reply; 10+ messages in thread
From: Martín Hötzel Escardó @ 2019-01-10 13:53 UTC (permalink / raw)
  To: Homotopy Type Theory


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

You will find answers in the blog post by Anders Mortberg:

https://homotopytypetheory.org/2018/12/06/cubical-agda/

Martin


On Thursday, 10 January 2019 13:37:33 UTC, Ali Caglayan wrote:
>
> I just noticed that [agda supposedly has support for HITs](
> https://github.com/agda/agda/issues/2761) since November. Since I didn't 
> realise this was the case I am letting people here know too.
>
> Now my questions:
>
> Are these really HITs? 
>
> Do they work without axiom K? 
>
> What can and can't be done with them?
>

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

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

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

* [HoTT] Re: HITs in Agda
  2019-01-10 13:53 ` [HoTT] " Martín Hötzel Escardó
@ 2019-01-10 15:19   ` Ali Caglayan
  2019-01-10 15:28     ` Nils Anders Danielsson
  0 siblings, 1 reply; 10+ messages in thread
From: Ali Caglayan @ 2019-01-10 15:19 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I was under the impression that this was in plain agda, that's why it was 
more suprising. I didn't realise it was about the cubical agda.

On Thursday, 10 January 2019 13:53:19 UTC, Martín Hötzel Escardó wrote:
>
> You will find answers in the blog post by Anders Mortberg:
>
> https://homotopytypetheory.org/2018/12/06/cubical-agda/
>
> Martin
>
>
> On Thursday, 10 January 2019 13:37:33 UTC, Ali Caglayan wrote:
>>
>> I just noticed that [agda supposedly has support for HITs](
>> https://github.com/agda/agda/issues/2761) since November. Since I didn't 
>> realise this was the case I am letting people here know too.
>>
>> Now my questions:
>>
>> Are these really HITs? 
>>
>> Do they work without axiom K? 
>>
>> What can and can't be done with them?
>>
>

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

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 15:19   ` Ali Caglayan
@ 2019-01-10 15:28     ` Nils Anders Danielsson
  2019-01-10 20:54       ` Martín Hötzel Escardó
  0 siblings, 1 reply; 10+ messages in thread
From: Nils Anders Danielsson @ 2019-01-10 15:28 UTC (permalink / raw)
  To: Ali Caglayan, Homotopy Type Theory

On 10/01/2019 16.19, Ali Caglayan wrote:
> I was under the impression that this was in plain agda, that's why it
> was more suprising. I didn't realise it was about the cubical agda.

You get Cubical Agda by using the option --cubical (for instance in a
pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound
to import Agda code that uses --without-K from Cubical Agda.

-- 
/NAD

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

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

* [HoTT] Re: HITs in Agda
  2019-01-10 13:37 [HoTT] HITs in Agda Ali Caglayan
  2019-01-10 13:53 ` [HoTT] " Martín Hötzel Escardó
@ 2019-01-10 20:53 ` Martín Hötzel Escardó
  1 sibling, 0 replies; 10+ messages in thread
From: Martín Hötzel Escardó @ 2019-01-10 20:53 UTC (permalink / raw)
  To: Homotopy Type Theory


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



On Thursday, 10 January 2019 13:37:33 UTC, Ali Caglayan wrote:
>
> I just noticed that [agda supposedly has support for HITs](
> https://github.com/agda/agda/issues/2761) since November. Since I didn't 
> realise this was the case I am letting people here know too.
>
> Now my questions:
>
> Are these really HITs? 
>
> Do they work without axiom K? 
>
> What can and can't be done with them?
>

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

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 15:28     ` Nils Anders Danielsson
@ 2019-01-10 20:54       ` Martín Hötzel Escardó
  2019-01-10 21:04         ` Evan Cavallo
                           ` (2 more replies)
  0 siblings, 3 replies; 10+ messages in thread
From: Martín Hötzel Escardó @ 2019-01-10 20:54 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Actually, I think it is not a priori clear how Agda's --without-K interacts 
with --cubical.

For one thing, the cubical identity type (derived from the cubical path 
type via Andrew Swan's technique) is not an Agda inductive family and it is 
not Agda's inductively defined identity type. And also, as far as I know, 
inductive families RE an open problem in cubical type theory / the cubical 
model(s).

Any development in Agda invoking --cubical that tries to be sound should, 
for the moment, refrain from using inductive families.

In fact, in would be good to discuss the precautions one should take when 
using --cubical in Agda so that one is guaranteed to be consistent, and 
better, be talking about something that is currently understood (such as 
entities in the cubical model((s)). It is not entirely clear to me which 
features of Agda we can use and which ones we should not use and which ones 
we could use if we knew more.

Martin

On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders Danielsson wrote:
>
> On 10/01/2019 16.19, Ali Caglayan wrote: 
> > I was under the impression that this was in plain agda, that's why it 
> > was more suprising. I didn't realise it was about the cubical agda. 
>
> You get Cubical Agda by using the option --cubical (for instance in a 
> pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound 
> to import Agda code that uses --without-K from Cubical Agda. 
>
> -- 
> /NAD 
>

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

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 20:54       ` Martín Hötzel Escardó
@ 2019-01-10 21:04         ` Evan Cavallo
  2019-01-10 21:37           ` Martín Hötzel Escardó
  2019-01-11 11:48         ` Nils Anders Danielsson
  2019-01-14 22:48         ` Thorsten Altenkirch
  2 siblings, 1 reply; 10+ messages in thread
From: Evan Cavallo @ 2019-01-10 21:04 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

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

Hi all,

Our recent paper explains how to handle inductive families in cartesian
cubical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf. We
believe something similar will work for De Morgan cubical type theory, and
I think Andrea and Anders are planning to work that out and add it to
cubical Agda. For the moment it looks like cubical Agda will let you
declare inductive families, but will not reduce the Kan operations in those
types.

Evan

2019年1月10日(木) 15:54 Martín Hötzel Escardó <escardo.martin@gmail.com>:

> Actually, I think it is not a priori clear how Agda's --without-K
> interacts with --cubical.
>
> For one thing, the cubical identity type (derived from the cubical path
> type via Andrew Swan's technique) is not an Agda inductive family and it is
> not Agda's inductively defined identity type. And also, as far as I know,
> inductive families RE an open problem in cubical type theory / the cubical
> model(s).
>
> Any development in Agda invoking --cubical that tries to be sound should,
> for the moment, refrain from using inductive families.
>
> In fact, in would be good to discuss the precautions one should take when
> using --cubical in Agda so that one is guaranteed to be consistent, and
> better, be talking about something that is currently understood (such as
> entities in the cubical model((s)). It is not entirely clear to me which
> features of Agda we can use and which ones we should not use and which ones
> we could use if we knew more.
>
> Martin
>
> On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders Danielsson wrote:
>>
>> On 10/01/2019 16.19, Ali Caglayan wrote:
>> > I was under the impression that this was in plain agda, that's why it
>> > was more suprising. I didn't realise it was about the cubical agda.
>>
>> You get Cubical Agda by using the option --cubical (for instance in a
>> pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound
>> to import Agda code that uses --without-K from Cubical Agda.
>>
>> --
>> /NAD
>>
> --
> 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.
> 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.
For more options, visit https://groups.google.com/d/optout.

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 21:04         ` Evan Cavallo
@ 2019-01-10 21:37           ` Martín Hötzel Escardó
  0 siblings, 0 replies; 10+ messages in thread
From: Martín Hötzel Escardó @ 2019-01-10 21:37 UTC (permalink / raw)
  To: Homotopy Type Theory


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



On Thursday, 10 January 2019 21:05:09 UTC, E Cavallo wrote:
>
> Our recent paper explains how to handle inductive families in cartesian 
> cubical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf. 
>

Nice.
 

> We believe something similar will work for De Morgan cubical type theory, 
> and I think Andrea and Anders are planning to work that out and add it to 
> cubical Agda. 
>

This is good too.
 

> For the moment it looks like cubical Agda will let you declare inductive 
> families, but will not reduce the Kan operations in those types.
>

Right. For the moment, you can prove that Agda's identity type (defined as 
an inductive family) is equivalent to the cubical identity type (because 
both have refl and J). However, the computations get stuck.

In fact, I tried this in order to be able to use Agda's pattern macthing on 
refl, rather than J on the cubical identity type, by going back-and-forth, 
but, as you say, the computations get stuck. 

If you manage to get the computations to go through, as you discuss above, 
with the work of Andreas and Anders, then this means that we can start 
using pattern matching on refl in cubical Agda without having to change 
Agda in any way other than accounting for inductive families (by the back 
and forth trick).
That would be nice for me, because what is preventing me from migrating 
from Agda to cubical Agda in my univalent development is that fact that it 
is populated by definitions by pattern matching on refl (and everything 
else) everywhere (according to the Agda style). 

So I am looking forward to the outcome of the developments you are 
advertising.

Martin

 

> Evan
>
> 2019年1月10日(木) 15:54 Martín Hötzel Escardó <escardo...@gmail.com 
> <javascript:>>:
>
>> Actually, I think it is not a priori clear how Agda's --without-K 
>> interacts with --cubical.
>>
>> For one thing, the cubical identity type (derived from the cubical path 
>> type via Andrew Swan's technique) is not an Agda inductive family and it is 
>> not Agda's inductively defined identity type. And also, as far as I know, 
>> inductive families RE an open problem in cubical type theory / the cubical 
>> model(s).
>>
>> Any development in Agda invoking --cubical that tries to be sound should, 
>> for the moment, refrain from using inductive families.
>>
>> In fact, in would be good to discuss the precautions one should take when 
>> using --cubical in Agda so that one is guaranteed to be consistent, and 
>> better, be talking about something that is currently understood (such as 
>> entities in the cubical model((s)). It is not entirely clear to me which 
>> features of Agda we can use and which ones we should not use and which ones 
>> we could use if we knew more.
>>
>> Martin
>>
>> On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders Danielsson wrote:
>>>
>>> On 10/01/2019 16.19, Ali Caglayan wrote: 
>>> > I was under the impression that this was in plain agda, that's why it 
>>> > was more suprising. I didn't realise it was about the cubical agda. 
>>>
>>> You get Cubical Agda by using the option --cubical (for instance in a 
>>> pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound 
>>> to import Agda code that uses --without-K from Cubical Agda. 
>>>
>>> -- 
>>> /NAD 
>>>
>> -- 
>> 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 <javascript:>.
>> 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.
For more options, visit https://groups.google.com/d/optout.

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 20:54       ` Martín Hötzel Escardó
  2019-01-10 21:04         ` Evan Cavallo
@ 2019-01-11 11:48         ` Nils Anders Danielsson
  2019-01-14 22:48         ` Thorsten Altenkirch
  2 siblings, 0 replies; 10+ messages in thread
From: Nils Anders Danielsson @ 2019-01-11 11:48 UTC (permalink / raw)
  To: Homotopy Type Theory

On 10/01/2019 21.54, Martín Hötzel Escardó wrote:
> Actually, I think it is not a priori clear how Agda's --without-K
> interacts with --cubical.

When I wrote that "The idea is that it should be sound to import Agda
code that uses --without-K from Cubical Agda" I didn't mean to imply
that there are any guarantees, or that there are no known problems with
the current implementation.

-- 
/NAD

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

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

* Re: [HoTT] Re: HITs in Agda
  2019-01-10 20:54       ` Martín Hötzel Escardó
  2019-01-10 21:04         ` Evan Cavallo
  2019-01-11 11:48         ` Nils Anders Danielsson
@ 2019-01-14 22:48         ` Thorsten Altenkirch
  2 siblings, 0 replies; 10+ messages in thread
From: Thorsten Altenkirch @ 2019-01-14 22:48 UTC (permalink / raw)
  To: Martín Hötzel Escardó, Homotopy Type Theory

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

I started working on this with Andrea at the Agda Implementer’s meeting. The idea is that you can add a constructor for transp to your inductive families but then reduce it to during pattern matching. This is similar to the way comp is implemented now. In the case of the equality type that should give you a type which is isomorphic to the path type but intentionally behaves differently, in particular J-beta holds. This is an alternative to Andrew Swan’s solution, I think.

Cheers,
Thorsten

From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com>
Date: Friday, 11 January 2019 at 07:54
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Re: HITs in Agda

Actually, I think it is not a priori clear how Agda's --without-K interacts with --cubical.

For one thing, the cubical identity type (derived from the cubical path type via Andrew Swan's technique) is not an Agda inductive family and it is not Agda's inductively defined identity type. And also, as far as I know, inductive families RE an open problem in cubical type theory / the cubical model(s).

Any development in Agda invoking --cubical that tries to be sound should, for the moment, refrain from using inductive families.

In fact, in would be good to discuss the precautions one should take when using --cubical in Agda so that one is guaranteed to be consistent, and better, be talking about something that is currently understood (such as entities in the cubical model((s)). It is not entirely clear to me which features of Agda we can use and which ones we should not use and which ones we could use if we knew more.

Martin

On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders Danielsson wrote:
On 10/01/2019 16.19, Ali Caglayan wrote:
> I was under the impression that this was in plain agda, that's why it
> was more suprising. I didn't realise it was about the cubical agda.

You get Cubical Agda by using the option --cubical (for instance in a
pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound
to import Agda code that uses --without-K from Cubical Agda.

--
/NAD
--
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>.
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.
For more options, visit https://groups.google.com/d/optout.

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

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

end of thread, other threads:[~2019-01-14 22:48 UTC | newest]

Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-01-10 13:37 [HoTT] HITs in Agda Ali Caglayan
2019-01-10 13:53 ` [HoTT] " Martín Hötzel Escardó
2019-01-10 15:19   ` Ali Caglayan
2019-01-10 15:28     ` Nils Anders Danielsson
2019-01-10 20:54       ` Martín Hötzel Escardó
2019-01-10 21:04         ` Evan Cavallo
2019-01-10 21:37           ` Martín Hötzel Escardó
2019-01-11 11:48         ` Nils Anders Danielsson
2019-01-14 22:48         ` Thorsten Altenkirch
2019-01-10 20:53 ` Martín Hötzel Escardó

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