Zulip Chat Archive

Stream: general

Topic: Set.mk

Violeta Hernández (Jul 14 2022 at 21:56):

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 (Jul 15 2022 at 08:52):

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 (Jul 15 2022 at 16:04):

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 (Jul 15 2022 at 16:56):

Most other types already do this

Eric Wieser (Jul 15 2022 at 16:56):

Often because they bundle the constructor as a morphism

Last updated: Aug 03 2023 at 10:10 UTC