Eventuality in a Net

Let $f:D\to X$ be a Net in a type $X$, and let $P:X\to\Omega$ be a predicate on $X$. We say that $P$ eventually holds on the net $f$ if

• $\exists(i:D).\;\forall(j:D).\;i\leq j\Rightarrow P(f(j))$

This is a topological manifestation of an Eventuality Modality, where we view the predicate $P:X\to\Omega$ as an $X$-parameterized proposition, and the net $f$ as a particular timeline.

Properties

• Eventuality in a net is dual to Necessity in a Net.