Nils Anders Danielsson

> For the 2.6.3 release, I think the cleanest option is to lock support for cubical indexed inductives behind a flag Should that flag be compatible with `--safe`?

If the only problem is that Agda might crash, then I think it is fine to make the flag compatible with `--safe`. The idea of that flag is that when...

What is "operator reconstruction"? In cases where two distinct expressions are printed in the same way I think it makes sense to find some way to explain how they differ....

If we do not try to check that the right error is triggered, then the semantics of this feature is presumably a bit less complicated. I guess that the informal...

When it comes to the syntax I think I would prefer a block keyword to a pragma. I guess other systems support this kind of thing. What notation do they...

The use case that was discussed in #3374 was writing tutorials using literate Agda. For this use case I think we could live without checking that the right error message...

Can you give an example of what you want to do?

> ```agda > module _ (A : Set) where > data List : Set where > nil : List > cons : A -> List -> List > > _++_...

> (let's call it **subinjective** as it is usable on definitions whose type is injective) Should the keyword only apply to certain definitions, or do you mean that it would...

Some comments: * Should the keyword apply only to the innermost module, or also to outer ones? * What does the proposed keyword `subinjective` have to do with "make certain...