Zulip Chat Archive

Stream: general

Topic: classes Type or Prop


view this post on Zulip Reid Barton (Apr 26 2018 at 22:42):

Is there any particular reason not to make t2_space and similar classes a Prop?

class t2_space (α : Type u) [topological_space α] :=
(t2 : x y, x  y  u v : set α, is_open u  is_open v  x  u  y  v  u  v = )

view this post on Zulip Reid Barton (Apr 26 2018 at 22:42):

I actually had sort of assumed that a structure with only Prop fields would automatically be a Prop by default.

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 22:59):

I noticed earlier this week that this wasn't happening

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 23:00):

As I'm sure you know, if you are defining your own class you can just tell it to be a Prop

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 23:00):

but that won't help you here

view this post on Zulip Reid Barton (Apr 26 2018 at 23:05):

I don't really need it to be a Prop, I just tried to use it as a Prop and was surprised when it didn't work, but it's easy enough for me to avoid doing that.

view this post on Zulip Reid Barton (Apr 26 2018 at 23:06):

I came across this comment later in the same file which makes me think the statuses of these structures are a bit accidental:

/- countability axioms

For our applications we are interested that there exists a countable basis, but we do not need the
concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
-/

view this post on Zulip Reid Barton (Apr 26 2018 at 23:07):

(It's followed by a structure which is indeed declared to be a Prop.)

view this post on Zulip Mario Carneiro (Apr 27 2018 at 01:05):

I think that's a typo. I'll change it


Last updated: May 11 2021 at 00:31 UTC