Homotopy Type Theory Sandbox (Rev #2, changes)

\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:

The filter

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.