Amélia

I think we can come up with a better syntax for https://github.com/agda/cubical/pull/1153?

while we're at it, do we have a need for total-hom over sigma? i don't like it— i also think we should get rid of the named record contractors in...

You can do [`env AGDA=/what/ever AGDAFLAGS='whatever' bash support/check.sh`](https://github.com/plt-amy/1lab/blob/main/support/check.sh)

To summarize the discussion there/our findings from the AIM, the issue is essentially that keeping around the telescopes for solved (primarily instance) metas in macros leads to quadratic duplication of...

AIUI the problem isn't in the generated terms, but rather in the macros themselves — the duplicated intermediate results are present in meta telescopes in suspended computations (after using e.g....

If we change the macro call to print the type of `DC` instead of normalizing it we get some nonsense: ```agda {n : Nat} → D (.HasCast.cast HasCast-Nat (1 ,...

So that code *is* nonsense but it's nonsense in an extremely subtle way (not the way I thought): `Test244.theNat` indeed is parametrised over the generalisation telescope, so that's not the...

Don't close it though. The "fix" is at the expense of a huge performance loss.