Zulip Chat Archive

Stream: new members

Topic: subtype is just a structure?


view this post on Zulip 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}

view this post on Zulip Johan Commelin (Feb 24 2021 at 18:38):

It's just notation on top of a structure

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 18:41):

subtype.property

view this post on Zulip Eric Wieser (Feb 24 2021 at 18:49):

docs#subtype.prop is often syntactically the better form

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Feb 24 2021 at 19:00):

The latter

view this post on Zulip Eric Wieser (Feb 24 2021 at 19:00):

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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Feb 24 2021 at 19:03):

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

view this post on Zulip Eric Wieser (Feb 24 2021 at 19:15):

Oh, but funext isn't an axiom!


Last updated: May 15 2021 at 00:39 UTC