analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
Recall (here) that a setoid may be understood as a thin (0,1)-dagger category, hence as a thin dagger-category enriched over the cartesian monoidal proset of truth values. In generalization, one may speak of enriching preorders over other monoidal posets.
Let $(M, \leq, \otimes, 1)$ be a monoidal poset. A $M$-enriched setoid or setoid enriched over/in $M$ is a set $P$ with a binary function $o:P \times P \to M$ such that
for every $a \in P$, $b \in P$, and $c \in P$, $o(a, b) \otimes o(b, c) \leq o(a, c)$
for every $a \in P$ and $b \in P$, $o(a, b) \leq o(b, a)$
for every $a \in P$, $1 \leq o(a, a)$
An $M$-enriched univalent setoid is an $M$-enriched setoid which additinally satisfies $1 \leq o(a, b) \Rightarrow a = b$.
For $M$-enriched univalent setoids, $o(a, b) = o(b, a)$, $o(a, a) = 1$, and $1 = o(a, b) \Rightarrow a = b$.
An ordinary setoid is just an $\Omega$-enriched setoid, with $\Omega$ the set of truth values.
A pseudometric space is a $(\mathbb{R}_{\geq 0}, \geq, +, 0)$-enriched setoid, where $\mathbb{R}_{\geq 0}$ are the non-negative Dedekind real numbers.
A metric space is a $(\mathbb{R}_{\geq 0}, \geq, +, 0)$-enriched set/univalent setoid, where $\mathbb{R}_{\geq 0}$ are the non-negative Dedekind real numbers.
Given any Archimedean integral domain $A$ and an Archimedean integral subdomain $B \subseteq A$, then $B$ is an $(A_{\geq 0}, \geq, +, 0)$-enriched set, where $A_{\geq 0}$ is the non-negative elements of $A$.
A set with an apartness relation is an $\Omega^\op$-enriched setoid, where the co-Heyting algebra $\Omega^\op$ is the opposite poset of the set of truth values $\Omega$.
Last revised on May 30, 2022 at 20:50:42. See the history of this page for a list of all contributions to it.