Zulip Chat Archive

Stream: maths

Topic: ultrafilters


view this post on Zulip 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?

view this post on Zulip Reid Barton (Oct 18 2018 at 23:05):

I assume naming it β won't fly

view this post on Zulip Reid Barton (Oct 18 2018 at 23:39):

Would it be okay to rename ultrafilter to is_ultrafilter?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:39):

I think so

view this post on Zulip Reid Barton (Oct 18 2018 at 23:40):

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

view this post on Zulip Reid Barton (Oct 18 2018 at 23:41):

I guess I should just say "subtype"

view this post on Zulip Johannes Hölzl (Oct 19 2018 at 07:14):

renaming ultrafilter to is_ultrafilter is fine for me.

view this post on Zulip Johan Commelin (Oct 19 2018 at 07:17):

Alternatively, you could have called it Ultrafilter...


Last updated: May 06 2021 at 19:30 UTC