Homotopy Type Theory Sandbox (changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

~~\tableofcontents~~ metric spaces

~~Propositions and subtypes~~

reflexive: for all $x \in S$ and $\epsilon \in \mathbb{R}_+$ , $x \sim_\epsilon x$ .
symmetric: for all $x \in S$ , $y \in S$ , and $\epsilon \in \mathbb{R}_+$ , $x \sim_\epsilon y$ implies that $y \sim_\epsilon x$ .
additively transitive: for all $x \in S$ , $y \in S$ , $z \in S$ , $\epsilon \in \mathbb{R}_+$ , and $\delta \in \mathbb{R}_+$ , $x \sim_\epsilon y$ and $y \sim_\delta z$ implies that $x \sim_{\epsilon + \delta} z$ .
separation: for all $x \in S$ and $y \in S$ , if $x \sim_\epsilon y$ for all $\epsilon \in \mathbb{R}_+$ , then $x = y$ .

~~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.~~

Last revised on November 18, 2024 at 18:07:35. See the history of this page for a list of all contributions to it.