Nils Anders Danielsson

Agda currently displays `Checked` in the mode line when a buffer has been successfully type-checked. One could perhaps display something like `Running` while a command is in progress. If you...

I added this to the icebox milestone. That does not mean that I think it is a bad idea, but I don't plan to work on it.

> In particular, I haven't figured out any way to debug what's going on during the application of rewrite rules. I have little experience of using rewrite rules, but I...

[Apparently](https://www.collabora.com/news-and-blog/blog/2020/08/27/using-the-linux-kernel-case-insensitive-feature-in-ext4/) some recent Linux kernel supports file systems for which `floß` and `FLOSS` refer to the same file. What is the goal with Agda's support for case-insensitive file systems? One...

> That sounds too complicated. ``` ghci> :set -XOverloadedStrings ghci> :set -package text-icu package flags have changed, resetting and loading new packages... ghci> import Data.Text.ICU ghci> toCaseFold False "FLOSS" ==...

Perhaps one should first normalise: ``` ghci> "ö" == "ö" False ghci> toCaseFold False "ö" == toCaseFold False "ö" False ghci> normalize NFD "ö" == normalize NFD "ö" True ```

This doesn't sound so bad: > * Disable ```Glue``` Easy. > * Restrict to only set-truncated HITs I suppose one way to do this would be to check that at...

> OK, once that change has been implemented I suggest that we also implement "`--cubical-with-uip`". That is a bad name choice, I want something that is consistent with both UIP...

Some questions: * The idea is that the proposed new variant of Agda should be compatible with UIP. Would it be compatible with `--with-K`? * What about propositional extensionality/univalence for...

@Saizan, have you thought about my two questions [above](https://github.com/agda/agda/issues/3750#issuecomment-496490806)?