set or subtype

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

In general, when should one use set or subtype to encode what are done by using sets on paper? Also, I found @[instance] def set.has_coe_to_sort {α : Type u_1} : has_coe_to_sort (set α) in mathlib, but how can one go the other direction, i.e., from subtypes to sets?

[Kyle Miller]

I can't really answer this this due to inexperience, but here are a few observations.

The definitions of set and subtype are as follows:

universes u

def set (α : Type u) := α → Prop

structure subtype {α : Sort u} (p : α → Prop) := (val : α) (property : p val)

A set is merely a predicate on a particular type, and x ∈ s is notation for s x, which is to say the predicate is true for x. A subtype, however, consists of pairs of an element of the type along with a proof that it satisfies a fixed property. So, you can write x : subtype α p with the : notation. The coersion you mention lets you use sets in place of types; in particular, if s and s' are sets, you can write f : s → s', and it will coerce these sets to subtypes automatically.

Sets and subtypes have the following sort of inverse pair:

def prop₁ {α : Type u} (s : set α) (x : α) (h : x ∈ s) : subtype s := ⟨x, h⟩
def prop₂ {α : Type u} (s : set α) (x : subtype s) : (x.val ∈ s) := x.property

So, an element of a subtype is an element x : α along with a proof of x ∈ s.

Interestingly, the definition of ∃ is

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

While this uses Sort rather than Type (allowing α to be Prop) and looks nearly the same as subtype, a key difference is that an Exists is a Prop rather than a Type u. Because of proof irrelevance, two instances of Exists are equal even if their w values are different. In contrast, two instances of subtype are equal iff their val members are equal (note: proof irrelevance means the property proofs don't come into the equality test).

[Kyle Miller]

In fact, it appears subtype itself is the coersion from sets to types. Given a set s : set α, then, since s is just a predicate, subtype s is a type consisting of all pairs ⟨x, h⟩ with x : α and h : x ∈ s.

The standard library has the definition

instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩

but it could just as well be

instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, subtype⟩

[Kevin Buzzard]

A (sub)set is a term, not a type. It doesn't have terms, but it has elements. A subtype is a type. They're two different ways of carrying the same concepts around

[Kyle Miller]

Also, consider a category whose objects are given by all the types in a universe (terms of Type u) and whose morphism sets are the functions between these types. The Prop type pretty much gives a subobject classifier. Given an object α and a function f : α → Prop, one can consider the preimage of true as a subset of α (called a set in Lean). The subtype type constructor gives an object subtype f that has a monomorphism subtype f → α whose image is exactly that preimage.

If you're wanting to work with this full category, it seems like it's better to use subtypes than sets. However, for local reasoning sets seem to be rather useful. (That said, if s is a set, then ↑s is subtype s, and if you've got h : x ∈ s in your context, then it's easy enough to bundle together an element ⟨x, h⟩ : ↑x. So you're not limiting yourself by using sets.)

[Kevin Buzzard]

One of the most important, and most confusing, basic things to internalise, is that the type set X is the type of subsets of X, but it is called neither subset X or powerset X

[Kyle Miller]

Yeah, that took me a bit of mental reconfiguration. My first non-confusing way of thinking about it was that it's like the category of sets with "universe" X, though the analogy is lacking since set X doesn't have any of the functions between sets. Something I found helpful thinking about is the axiom of separation and how subsets "are" the extension of a predicate.

(Where the analogy is also lacking is it seems there shouldn't be an X where set X "is" $\mathsf{Set}$. To "be" this category, what we'd want is for every term of set X to have a corresponding term of X, but you seem to get a Russell's paradox. Not to mention there being a set that contains itself in the form of (λ x, true) : set X, so it would violate the axiom of regularity.)

[Kevin Buzzard]

Right: a subset of X is the same as a function X -> Prop. I think it's difficult to imagine the category of all sets in this way, because you can't have an abstract set in type theory, you can only have a subset of X, and X is a type so its "elements" (terms) don't have elements.

[Kyle Miller]

I guess what I was thinking is how you can sometimes have internal versions of different constructions. There might have been functions f : set X → X and mem : X → X → Prop with the property that x ∈ s ↔ mem x (f s) for every x : X and s : set X, but now that I think about it cardinality prevents this possibility. (So this sort of thing can't possibly work for at least three different reasons now :grinning:. However... if you only use definable sets I'm unsure whether this is impossible, though likely f wouldn't be anything computable.)