Andreas Abel

> > * We should make up our mind whether we use dash-style keywords or CaMl-case. It seems that recent keywords have been added in dash-style, so I'd prefer `unquote-decl`....

Well, yeah, I suppose we need to have a deprecation process for the caml-case keywords. Does not necessarily have to be coupled with your PR, so be free to stick...

Discussion entry (dev meeting 2022-04-13): `unquoteDecl` could be generalized to take scope-versions of arbitrary declarations, followed by an expression which delivers these at type-checking time (using reflection). Syntax draft: ```agda...

Do you need more builtins on the Agda side for this? (There are no NATMAX, NATMIN etc. builtins atm.)

> The fishiest thing to me is the definition of `Embed`, which seems like it should belong to `Set₁` instead of `Set`. It would appear that Agda treats `A` like...

Here is a small simplification (eliding the data type `Bad`, making sizes explicit): ```agda {-# OPTIONS --sized-types #-} open import Agda.Builtin.Size record Thunk (F : Size → Set₁) i :...

The fact that `A` is _forced_ in the constructor of `Embed` lets it skip the universe check: https://github.com/agda/agda/blob/5d2d77abbc0c97f5b23d7089797c3ef8796508dc/src/full/Agda/TypeChecking/Rules/Data.hs#L1750-L1753 The rationale was that you cannot project out `A` from a value...

Final shrinking: ```agda {-# OPTIONS --sized-types #-} open import Agda.Builtin.Size -- T i ≈ Set with a fake size dependency. -- We have Set → T i but T i...

But these names are ambiguous, no?

Background: #2604.