subset or subtype?

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

First is

[Kevin Buzzard]

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

[Kevin Buzzard]

Second is

[Kevin Buzzard]

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

[Kevin Buzzard]

Which is "better"?

[Kevin Buzzard]

I seem to be able to work with either

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

which is which ;-)

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

so it can be used more easily as a target

[Kevin Buzzard]

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]

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]

(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.)