## Stream: general

### Topic: subset or subtype?

#### 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.

First is

#### Kevin Buzzard (Mar 04 2018 at 17:16):

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

Second is

#### Kevin Buzzard (Mar 04 2018 at 17:17):

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

#### Kevin Buzzard (Mar 04 2018 at 17:17):

Which is "better"?

#### Kevin Buzzard (Mar 04 2018 at 17:17):

I seem to be able to work with either

#### 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?

#### Gabriel Ebner (Mar 04 2018 at 17:21):

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

#### Kevin Buzzard (Mar 04 2018 at 17:22):

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

#### Patrick Massot (Mar 04 2018 at 17:22):

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

#### Kevin Buzzard (Mar 04 2018 at 17:22):

which is which ;-)

#### 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

#### 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.

#### Kevin Buzzard (Mar 04 2018 at 17:23):

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

#### Kevin Buzzard (Mar 04 2018 at 17:23):

so it can be used more easily as a target

#### 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

#### 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.

#### 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