\tableofcontents ## Propositions and subtypes ## Filters ## Free ultrafilters ## Pretopological spaces A pretopological space consists of a type $S$ with a relation $F \to x$ between the type of filters on $S$, $F:\mathrm{Filters}(S)$ and $S$, $x:S$, which is * Centred: Given an element $x:S$, the free ultrafilter of $x$ converges to $x$. * Isotone: Given an element $x:S$, if $F$ converges to $x$ and $F$ is a subtype of $G$, then $G$ converges to $x$ * Infinitely directed: Given an element $x:S$, the intersection of all filters which converge to $x$ also converges to x: $$\left(\bigcap_{G:\sum_{F:\mathrm{Filters}(S)} F \to x} \pi_1(G)\right) \to x$$ The filter $$\left(\bigcap_{G:\sum_{F:\mathrm{Filters}(S)} F \to x} \pi_1(G)\right)$$ is called the **neighbourhood filter** of $x$. We say that an element $x$ is in an open subset $U$ of $S$ if $U$ is in the neighbourhood filter of $x$. To do: define what a topological space is supposed to be in terms of the filter structure. [[!redirects Sandbox > history]]