## Stream: maths

### Topic: open_set

#### Reid Barton (Oct 09 2018 at 18:44):

@Scott Morrison I'm curious why you reversed the direction of the arrows of open_set. I would rather put the contravariant-ness in the notion of (pre)sheaf.

#### Scott Morrison (Oct 09 2018 at 21:30):

Ah, I hadn't seen this, and asked your opinion elsewhere. I'll reverse it again when I get there.

#### Kevin Buzzard (Oct 09 2018 at 21:59):

Yes Scott mentioned this before I think. Maybe he said something like he had ops everywhere at all times with no obvious purpose?

#### Kevin Buzzard (Oct 09 2018 at 21:59):

I guess the point is that we never use the unopped category

#### Johan Commelin (Oct 10 2018 at 01:25):

Right, but once we start doing sheaves over sites we will want contravariant (pre)sheaves. And we also want those to specialise to "plain old" (pre)sheaves on open sets. So I vote for keeping the op.

#### Kevin Buzzard (Oct 10 2018 at 06:07):

Another question of course is where you want the op -- source or target. It's funny this is coming up now. I distinctly remember Scott saying "eew there are ops everywhere, but I've had a brilliant idea -- if we just redefine the open set category then they all go away and it's much easier to use" and it was one of those moments where I just thought "yeah, it's not ideal but I can completely see his point. It removes all of them at once."

Last updated: May 14 2021 at 19:21 UTC