Matthias Ritter (formerly Hutzler)

> * Add a `.agda-lib` file for the builtin modules. This was previously attempted by @gallais here: https://github.com/agda/agda/pull/4616

I tried to search for unused imports recently: https://github.com/agda/cubical/pull/732 . I got the impression that there is currently no good automatic way of doing this. I tried [this tool](https://github.com/msuperdock/agda-unused), but...

Disclaimer: I am not familiar with nix flakes. :-) I successfully tested the flake by running: ```bash nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/7039feccf434861d16921522ebdf1bd2c3de5306 ``` @guilhermehas Could you perhaps provide a...

Thank you, @guilhermehas ! I agree that `INSTALL.md` would be a good place to put the usage example. Perhaps in a short section called "Nix flakes instructions"?

Also, a question about [.github/workflows/ci-nix.yml](https://github.com/agda/cubical/pull/800/files#diff-fb85e3427e423c8f80d79fb275a6683ccff2fe4340150528e54e389ea01445af): I assume that this CI job checks the whole library, as part of building the flake, which is already done by [ci-ubuntu.yml](https://github.com/agda/cubical/blob/master/.github/workflows/ci-ubuntu.yml). So does this...

I assume that the purpose of the Nix CI job is to check whether the (automatically generated) flake.lock file (which determines in particular the precise Agda version) needs to be...

The procedure in the new section in INSTALL.md works for me.

I wonder whether there is a more elegant definition for the open modality. But I can't find one, so I leave it like this for now.

I wonder if it could be best here to change the actual type signatures of `x≤y⊔x` and `x≤y⇒x≤z⊔y` (and similar cases) to reflect the order in which the variables x,...

No, I meant that there should be this: ```agda x≤y⊔x : ∀ x y → x ≤ y ⊔ x ``` This can not be achieved by a renaming-reexport of...