Ultrafilter monad
= Ultrafilter monad
{wiki}
The <ultrafilter functor> carries the monad structure obtained from its terminality among finite-coproduct-preserving endofunctors of sets. Its unit sends a point to its <principal ultrafilter>; its multiplication sends an ultrafilter of ultrafilters to the ultrafilter of subsets whose corresponding basic set of ultrafilters is large.