Have a look at "normalized types"

[gallais]

The Props are back in town! And there are some interesting use-cases: rocq-prover/rfcs#37 (comment)

This could be useful to implement data structures for which picking a unique representative
clashes with efficiency considerations (e.g. implementing a FIFO using two lists yields many
representations for the same FIFO but also guarantees amortised O(1) time for dequeue).

[HuStmpHrrr]

Is it -1-truncated/squashed type? Will Agda itself need to be changed too?

[gallais]

The current dev version of Agda has these props.