How do define a type isomorphic to an existing type?

Stream: general

[Daniel Weber]

I want to define the type of uniform distributions over a nonempty subset of the (finite) universe. It's isomorphic to nonempty finite sets of elements, but I want to be able to treat it as a PMF. I could work directly with the sets, but I'd like to be able to use them as functions.
What would be the nicest/most convenient to define this type? I thought about

{{a : PMF α // ∃ t, ∀ x, if x ∈ t then a x = 1 / (t.card : ℝ) else a x = 0}}

But this seems to hide the isomorphism too much–it requires proof that for any nonempty set, there's such a uniform distribution, proof that any such distribution has exactly one matching nonempty set, and that a distribution is equal to the distribution produced by its set. These aren't hard to prove, but is there a way to create this type which automatically gives those?

[Josha Dekker]

Are you familiar with uniformOfFinset in Probability/Distributions/Uniform.lean? (It also has uniformOfFintype and ofMultiset). They have some basic API. I also wrote the new uniformMeasure which might be useful (or not) to you, which is currently in #10456. There is a small part that is work-in-progress there, other than that I hope it should be available soon!