From IsPartition to IndexedPartition

Stream: Is there code for X?

[Felix Weilacher]

The docstring for docs#Data.Setoid.Partition says

"An indexed partition is a map s : ι → α whose image is a partition"

Do we have any sort of realization of this? Maybe something like the following? (Note the docstring is not quite right. s also needs to be injective.)

example {α β: Type*} (s : β → Set α) (h : Setoid.IsPartition (range s))  (h' : s.Injective) : IndexedPartition s