simp-normal form in `set_theory.cardinal`

Stream: maths

[Yury G. Kudryashov]

simp lemmas in set_theory.cardinal simplify, e.g., #α * #β to #(α×β), and similarly for other operations. This seems counter-intuitive for me. I think that simp should be able to compute cardinality of a complex type by applying simp lemmas (e.g., simplify #(nat → rat) to ω ^ ω). Any objections to a refactor?

[Yury G. Kudryashov]

@Mario Carneiro @Floris van Doorn :up:

[Mario Carneiro]

I agree, the simp lemma should go the other way there

[Floris van Doorn]

Yes, that seems good.

presumably the original motivation was "we just defined multiplication, how do we evaluate it on constructors," but the other way around makes more sense.