Amélia

Is #6770 a duplicate of this?

Does it work if you comment out the `instance _ : Dec ⊤`? The error message to me looks like a case of overlap (Agda refuses to decide between multiple...

I'm not sure I've _ever_ seen this feature used; it's not documented under record types _or_ instance arguments, either. I only became aware of it after @jespercockx pointed it out...

> I don't think there's any faulty behavior here, marking a field as an instance just turns the projection function into an instance, which is consistent with how _any other...

The generated `hcomp-T` and `transp-T` (*with* the dash!) are not redundant constructors, they are the "clause" that `hcomp` and `transp` will dispatch to, depending on what constructor is in the...

As for > Do you mean constructors in the literal sense, as technical term? It looks more like this is a function: @sattlerc is correct. Our formal `hcomp` and `transp`...

> I see, so I should not think of hcomp-T and transp-T as constructors in general [...] They're actually never constructors: these are the right-hand-side(s) of `hcomp {T} φ u...

Hum, the maths is redundant, but the explanation are better. Can we replace that for this?

- [ ] Syntax for small lists (must ponder: also for small vectors) - [ ] Range syntax for lists of naturals - [ ] Maybe have `Dec-eq`/`Dec-ord` _classes_???

To be clear I killed the save-metas run in this file because checking it successfully has max residency a bit over 1GiB: ``` 78,604,576,424 bytes allocated in the heap 9,346,647,992...