Homotopy Type Theory Sandbox (Rev #4, changes)

metric spaces

• 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$.