subtype

Stream: new members

[Alex Zhang]

Is it possible to prove that two subtypes are equal?

import data.fintype.card

variables {α β : Type*} (p q : α → Prop)

example (h: ∀ a, p a ↔ q a) : subtype p = subtype q :=
by {sorry}

[Eric Wieser]

Yes, first show p = q

[Eric Wieser]

Which you should be able to do by combining docs#propext and docs#funext

[Victor Porton]

Is there a notion of subtype (like subset)?

[Arthur Paulino]

If you scroll up this thread you'll see that there's indeed a subtype. It's defined in core as

/- Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description. -/
structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

But I'm not sure this is what you mean by "subtype"

[Eric Wieser]

(docs#subtype)

[Victor Porton]

@Arthur Paulino I mean subtype relation like subset relation.

[Victor Porton]

@Eric Wieser Not this.

[Eric Wieser]

Can you elaborate on what you mean?

[Kyle Miller]

The answer is "no" in the way you'd probably want -- every term has a type and only one type, and if you had subset-like subtypes you'd have to allow terms with more than one type.

Instead, what we have is that for every set (equivalently, every predicate on a type), there exists a type whose terms are, in some sense, in one-to-one correspondence with the elements of the set. There's an injective function from that type to the original type whose image consists of the elements of that set. One possible implementation of this type is subtype.

[Kyle Miller]

If you like to hear things like "subobject classifiers" I once posted a diagram.

[Kyle Miller]

In Lean/mathlib we use coercions to make it seem like subtype is a "subtype" in the sense you want, but you have to get used to it.

[Kyle Miller]

For example, when I write

example (s : set ℕ) (x : s) : ℕ := x

Lean is automatically inserting coercions so that it's actually

example (s : set ℕ) (x : subtype s) : ℕ := x.val

[Kyle Miller]

If you're wanting to consider more than one "subtype" of a type and relate them in different ways, it's usually less of a pain to work with sets, which, just to be clear, are just predicates on a type:

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