Ok so the past few days a lot of criticism of indexed inductives in #cubicalagda #agda has been going in and this is just my two cents from a user perspective but I defined (a datatype for lists indexed by the multisets of their elements)[http://partiallyapplied.eu/correct-bialgebraic-sorting/DistrLaw.html#1275] and successfully used it to define intrinsically correct sorting algorithms using bialgebraic semantics.
partiallyapplied.euDistrLaw
