equiv identifying sets

Stream: general

[Johan Commelin]

Suppose I have two types X Y : Type and an equiv e : equiv X Y. And suppose I have S : set X and T : set Y. I want to say that e identifies S with T. Now I can say that e.to_fun '' S = T, but that doesn't seem very symmetrical. Does it make sense to have some sort of predicate that takes an equiv and two sets for this job?

[Patrick Massot]

I guess it depends on the API you write for this predicate

[Kevin Buzzard]

Random related remark: I needed this when I was doing group_equiv; I wanted to prove that if group_equiv G H and K was a normal subgroup of G then group_equiv G/K H/K' where K' was the image of K. But it's not true in general that the image of a normal subgroup is a normal subgroup, so instead I had K a normal subgroup of G and proved group_equiv G/K' H/K where K' was defined to be the pre-image of K, which was known to be a normal subgroup.

[Chris Hughes]

Use preimages. They're much easier.