Zulip Chat Archive

Stream: general

Topic: subset or subtype?


view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:15):

I wrote presheaves of types twice in my life and I see now that my definitions differ.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:15):

First is

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:16):

(F : Π U : set α, T.is_open U → Type*)

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:17):

Second is

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:17):

(F : {U // topological_space.is_open T U} → Type*)

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:17):

Which is "better"?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:17):

I seem to be able to work with either

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:21):

Is the only difference that with the first I have two different names U and HU, and with the second I have V.val and V.property?

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 17:21):

Yes, it is analogous to the difference between A → B → C and A ∧ B → C.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:22):

But with those two choices, functional program people prefer the first, right?

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:22):

Proof assistant people seem to always prefer A → B → C, so which is better for presheaves?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:22):

which is which ;-)

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:22):

Presumably H.1 and H.2 is V.val and V.property so this is the one I should perhaps avoid

view this post on Zulip Reid Barton (Mar 04 2018 at 17:22):

The second one also gives you the name "V", which for doing abstract sheaf theory things (that don't care about the particular site) seems like it would be more convenient.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:23):

oh but here's a difference: A and B is a type

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:23):

so it can be used more easily as a target

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:27):

This doesn't seem to matter in practice. I am going for set because it seems to be analogous to the "more functional" A -> B -> C

view this post on Zulip Reid Barton (Mar 04 2018 at 17:36):

If you imagine defining a sheaf of sets on a general site, then the first way seems really unnatural (what would be the analogue of is_open?) So from a "math" perspective, the second way looks better.
I don't know what the practical implications are, though.

view this post on Zulip Reid Barton (Mar 04 2018 at 17:40):

(I would also set it up so that I can write U : T.open_set, and use \cap and \cup and \subset directly on open sets, etc.)


Last updated: May 10 2021 at 00:31 UTC