PR #15550: feat(set_theory/zfc/basic): `pSet` with empty ...

Stream: triage

[Random Issue Bot]

Today I chose PR 15550 for discussion!

feat(set_theory/zfc/basic): pSet with empty type is equivalent to Ø
Created by @Violeta Hernández (@vihdzp) on 2022-07-20
Labels: easy, awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

This is a recent one! I got stuck with @Eric Wieser on whether I should match docs#equiv.equiv_of_empty or ditch the extra equiv namespace.

[Violeta Hernández]

So ehm... what should I do?

[Mario Carneiro]

I think we usually don't use a namespace for that. equiv itself is maybe an exception because it doesn't want to pollute the global namespace, so I'm inclined to follow @Eric Wieser 's suggestion here