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