Name for ZFC `Set`

Stream: mathlib4

[Anatole Dedecker]

I'd like to port SetTheory.Zfc.Basic (it's not high on the list, but it looks fun!). However, I'm not quite sure what to make about the fact that we can't use capitalization as a distinguising feature anymore. Should I make Set protected as ZFC.Set? Or Zfc.Set? Or no namespace and just ZFSet?
@Mario Carneiro @Violeta Hernández

[Mario Carneiro]

ZFSet sounds good to me

[Mario Carneiro]

It should be ZFC not Zfc when it shows up in filenames and types btw

[Anatole Dedecker]

Yes that's what I was going to ask, Zfc feels wrong to me, but I didn't want to break anything in Mathport

[Reid Barton]

I guess this file wants the ordinary Set way too often for ZFC.Set to be a good alternative

[Anatole Dedecker]

I would have made it protected, so it was more of a readability question between a dot and no dot

[Anatole Dedecker]

Type for docs#pSet.type is obviously not a valid identifier. Is it fine if I replace it by Index? I know I could use «Type» but it sounds a bit painful when Index seems clear enough to me.

[Eric Wieser]

Isn't dot notation enough to make s.Type legal syntax?

[Eric Wieser]

protected ZFC.Set seems sensible to me, especially if there's something else that would belong in that namespace

[Yuyang Zhao]

There would be ZFC.Class, and in the future, there will also be ZFC.Ordinal.

[Eric Wieser]

That seems pretty convincing to me

[Anatole Dedecker]

Eric Wieser said:

Isn't dot notation enough to make s.Type legal syntax?

Yes when used like that it works, but there are still a couple places where you need to write «Type»