## 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?

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: May 06 2021 at 19:30 UTC