Necessity 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$ necessarily holds on the net $f$ if

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

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

Properties

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