Zulip Chat Archive

Stream: maths

Topic: ultrafilters

Reid Barton (Oct 18 2018 at 23:03):

I want to define the ultrafilter monad. I suppose this means I need a bundled type: filter plus the ultrafilter property. (Currently, we have ultrafilter : Π {α : Type u}, filter α → Prop.) Thoughts on naming?

Reid Barton (Oct 18 2018 at 23:05):

I assume naming it β won't fly

Reid Barton (Oct 18 2018 at 23:39):

Would it be okay to rename ultrafilter to is_ultrafilter?

Mario Carneiro (Oct 18 2018 at 23:39):

I think so

Reid Barton (Oct 18 2018 at 23:40):

otherwise, I'm having a hard time coming up with a name for the bundled thing

Reid Barton (Oct 18 2018 at 23:41):

I guess I should just say "subtype"

Johannes Hölzl (Oct 19 2018 at 07:14):

renaming ultrafilter to is_ultrafilter is fine for me.

Johan Commelin (Oct 19 2018 at 07:17):

Alternatively, you could have called it Ultrafilter...

Last updated: Dec 20 2023 at 11:08 UTC