The only examples of ultranets/ultrafilters described in Bourbaki and Willard are the trivial ones (generated by a single point). I know that their existence relies in general on the axiom of choice or the ultrafilter lemma.
I have two questions:
has any non-trivial ultranet been constructed?
is there any strong reason why no non-trivial ultranet has/will ever be constructed?