classes Type or Prop

Stream: general

[Reid Barton]

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]

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

[Kevin Buzzard]

I noticed earlier this week that this wasn't happening

[Kevin Buzzard]

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

[Kevin Buzzard]

but that won't help you here

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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