Nils Anders Danielsson

> ``` > Id : Type -> Type > Id a = a > ``` > > means `ω Id : Type -> Type`. But from the typing rule you're...

@andreasabel, @oskeri and I have studied a type theory with a configurable modality, and one conclusion is that it is not entirely straightforward to add linear types to Agda. For...

The following variant could also be considered: * If `--linearity` is used, then record types with η-equality and no fields or one or more erased fields are allowed, but only...

More things to consider (these things came up in a discussion with @plt-amy): * How should the new features interact with compile-time irrelevance? * How should the new features interact...

I've found several problems related to Cubical Agda. Problem 1 --------- Above I wrote that "we could perhaps get away with just having the current restriction for Π- and Σ-types...

> * Perhaps there is no good way to combine linear or affine types with Cubical Agda. In the presence of linear types one could perhaps restrict univalence to some...

I assume that you (indirectly) used `Cmd_compute UseShowInstance`, in which case this seems to be the intended behaviour: https://github.com/agda/agda/blob/a43f45ca661a5017c83754070394b2a755bb53dd/src/full/Agda/Interaction/BasicOps.hs#L365-L374

Can you give some more details of this feature?

Are there any restrictions on the type of a destructor? I guess that the record type that is being defined should be mentioned exactly once. Are there any restrictions on...

I sometimes use it when I'm not sure if something is a bug or not.