subtype is just a structure?

Stream: new members

[Vaibhav Karve]

I realized I can replicate subtype-functionality using a structure with two fields. Is there some advantage that subtypes offer which I am missing out on?

constant α : Type
constant predicate : α → Prop

structure A : Type :=
(val : α)
(property : predicate val)

def B : Type := {a : α // predicate a}

[Johan Commelin]

It's just notation on top of a structure

[Vaibhav Karve]

Thanks. Followup question: I can get back the predicate by referencing A.property by somehow I can't do this with B.property?

[Vaibhav Karve]

I tried (a : A).property and (b : B).property and in that case both seem to work fine.

[Yakov Pechersky]

subtype.property

[Eric Wieser]

docs#subtype.prop is often syntactically the better form

[Eric Wieser]

If using subtypes, you can show subtype p = subtype q if p iff q. Presumably the same type equality can't be achieved with two separate structures?

[Kyle Miller]

@Eric Wieser Do you mean the following lemma, or do you mean an equality between my_subtype and subtype?

structure my_subtype {α : Type*} (p : α → Prop) :=
(val : α)
(property : p val)

lemma eq_if_iff {α : Type*} (p q : α → Prop) (h : ∀ a, p a ↔ q a) :
  my_subtype p = my_subtype q :=
by rw (funext (λ a, propext (h a)) : p = q)

[Eric Wieser]

The latter

[Eric Wieser]

But that's a demo of the thing that I was saying was possible

[Kyle Miller]

Ok, I'm pretty sure the latter is unprovable. (Depending on the model, it'll either be true or false.)

[Eric Wieser]

I think it amounts to saying that two types are equal if they have the same recursive?

[Eric Wieser]

Which sounds like it would have to be axiomatic like docs#funext

[Eric Wieser]

Oh, but funext isn't an axiom!