Set.mk

Stream: general

[Violeta Hernández]

I'm wondering whether we should have docs#Set.mk instead of just using quotient.mk directly. There's not really any other setoids of interest we could possibly build out of pSet, and by using this custom definition, using rewrite lemmas like quotient.out_eq and quotient.eq just becomes more tedious.

[Floris van Doorn]

I think it's good practice to keep Set.mk. You probably only use a couple of results for quotients, and you can reformulate them for Set.

[Violeta Hernández]

Should we do this sort of thing for other types defined in terms of quotients, such as docs#game? We currently use quotient.mk throughout in its API.

[Eric Wieser]

Most other types already do this

[Eric Wieser]

Often because they bundle the constructor as a morphism