Re: [HoTT] Re: HITs in Agda

[Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>]

[-- 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 --]