## Stream: new members

### Topic: subtype is just a structure?

#### Vaibhav Karve (Feb 24 2021 at 18:37):

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 (Feb 24 2021 at 18:38):

It's just notation on top of a structure

#### Vaibhav Karve (Feb 24 2021 at 18:40):

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 (Feb 24 2021 at 18:41):

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

#### Yakov Pechersky (Feb 24 2021 at 18:41):

subtype.property

#### Eric Wieser (Feb 24 2021 at 18:49):

docs#subtype.prop is often syntactically the better form

#### Eric Wieser (Feb 24 2021 at 18:51):

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 (Feb 24 2021 at 18:58):

@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)


The latter

#### Eric Wieser (Feb 24 2021 at 19:00):

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

#### Kyle Miller (Feb 24 2021 at 19:02):

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

#### Eric Wieser (Feb 24 2021 at 19:02):

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

#### Eric Wieser (Feb 24 2021 at 19:03):

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

#### Eric Wieser (Feb 24 2021 at 19:15):

Oh, but funext isn't an axiom!

Last updated: May 15 2021 at 00:39 UTC