Amélia

Ah, we're being bitten in the behind by comp/transp taking a line of levels. Here's what @Saizan had to say on this when it last came up: https://github.com/agda/agda/issues/3722#issuecomment-556000316. I think...

Well, the extra duplication seems to happen only when `A` is in `Prop`: when it's in `Set`, they're deduplicated (the type signature looks like `∀ a (b b' : B...

I think `--experimental-transport-indices` is a good name: not too technical, describes exactly what goes wrong otherwise (substituting an index by a path will get stuck).

Without the flag, we'd skip: - Generating `transpX` for indexed families - Generating `trX-trX` clauses, `trX-hcomp` clauses, `trX-con` clauses when matching on indexed families That is: without the flag, we...

Something to keep in mind: #5448

Here's a summary of our discussion on this topic on 2022-08-31 (@jespercockx @andreasabel @nad @UlfNorell) to make sure we're all on the same page (and to get user feedback, of...

There are a fair number of subtleties around elaboration of modules that _could be_ loaded from Cubical Agda, particularly around indexed inductives — but, yes, also internal implementation details, as...

`--without-K` should also avoid generating `hcomp`/`transp` helpers for data types/records and the `transpX` constructors themselves.

I'm in GMT-3 (America/Sao_Paulo), and Wednesday works for me 🙂

@andreasabel What needs to be done re. > We should check for correct issue descriptions this?