## Stream: general

### Topic: classes Type or Prop

#### 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 = ∅)


#### 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.

#### Kevin Buzzard (Apr 26 2018 at 22:59):

I noticed earlier this week that this wasn't happening

#### 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

#### 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.

#### 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.
-/


#### Reid Barton (Apr 26 2018 at 23:07):

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

#### 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