Nils Anders Danielsson

I brought the code up to date. As part of that I made some [changes](https://github.com/agda/agda-stdlib/commit/ac34848cf847ecb1537c44e4d735c810e720312e) to the standard library (@vlopezj had already fixed one of the problems before, in a...

> One could start by repeating an experiment @vlopezj performed, in his words, "replacing the type of either the constraint or of the context variables by a blocked constant at...

As an experiment I replaced `__UNIMPLEMENTED__` with `selectSmaller direction (coerce twinLHS) (coerce twinRHS)` in `twinAt`. I don't expect this implementation to be entirely correct, but a number of test cases...

Such a mode should perhaps be enabled by default. Experienced users can turn it off if they want to. This can be somewhat awkward when switching between different versions of...

I asked the same thing, and @andreasabel had an [answer](https://github.com/agda/agda/issues/2756#issuecomment-387732467).

> Perhaps module IDs could be prefaced with `{module}` I'm working on this. > This kind of scheme could perhaps also be used to allow linking to private identifiers: `{private}`_private...

Is there a simple and efficient way to figure out if a `QName` was declared as a public or a private name?

I realised that the naming scheme outlined above does not work for record constructors (not even public ones): ```agda record R : Set₁ where constructor c field c : Set...

A larger test case: ```agda module _ where -- The top-level module does not count. module _ where private postulate A : Set -- 1.A module _ where private postulate...

> For the last identifier we have a choice: > * For uniformity we could go with `6.A`. > * There can only be one `A` in the top-level scope,...