basic constructions:
strong axioms
further
The concept of meros (plural meroi or meroses) is a relational analogue of that of a topos; where the morphisms in a topos are like functions, the morphisms in a meros are like relations. Like Set is the canonical base topos, so Rel is the archetypical meros. More generally, like topoi provide a context for generalized constructive set theory, so meroi provide a context for generalized relational set theory.
Where the boolean truth values of set theory are identified/generalized to elements of the subobject classifier of a topos, a meros instead represents Boolean values as degrees of inclusion between relations: between any two objects, there is a false relation (a zero morphism) and a true relation.
Following Kawahara 1995, we define an auxiliary venue for meroi first. An I-category is a dagger category where every hom-set has lattice structure. Specifically,
An I-category is a dagger category where, for all objects $A, B$, there is a partial order $\sqsubseteq$ on the morphisms $A \to B$, a least relation $0_{A,B}$ and greatest relation $\Theta_{A,B}$ such that
and the partial order commutes with the dagger structure:
I-categories can have a zero object like typical dagger categories, but also a terminal object.
When it exists, a terminal object in an I-category (Def. ) is an object $1$ such that $0_{1,1} \neq id_1 = \Theta_{1,1}$ and for all objects $A, B$, $\Theta_{1,B} \circ \Theta_{A,1} = \Theta_{A,B}$.
We next highlight specific morphisms within I-categories.
A morphism $f \colon A \to B$ in an I-category (Def. ) is called a partial function, or univalent, when $f \circ f^\dagger \sqsubseteq id_B$.
A partial function $f \colon A \to B$ (Def. ) is a total function, or function, when $id_A \sqsubseteq f^\dagger \circ f$.
A morphism $\alpha \colon A \to B$ in an I-category (Def. ) is rational when there exist functions $f \,\colon\, X \to A$ and $g \,\colon\, X \to B$ (in the sense of Def. ) such that $\alpha = g \circ f^\dagger$ and $f^\dagger \circ f \sqcap g^\dagger \circ g = id_X$.
For all $\alpha \,\colon\, A \to B, \beta \,\colon\, A \to C, \gamma \,\colon\, B \to C$ there exists a quotient $\beta \div \gamma \,\colon\, A \to B$ such that $\gamma \circ \alpha \sqsubseteq \beta \iff \alpha \sqsubseteq \beta \div \gamma$.
We also need the Dedekind formula, which relates any three morphisms between three objects.
We are now ready to define meroi. Instead of a lattice, we will now expect a complete Heyting algebra for each hom-set.
A meros is an I-category (Def. ) where:
The partial order $\sqsubseteq$ is not just a lattice, but a complete Heyting algebra.
The Dedekind formula (1) holds whenever possible.
There is a terminal object (in the sense of Def. ).
For all $\alpha \,,\, A \to B$ we have $0 \circ \alpha = \alpha \circ 0 = 0$.
$0 \sqsubseteq 0 \div \alpha \;\;\iff\;\; \alpha \circ 0 \sqsubseteq 0 \;\;\iff\;\; \alpha \circ 0 = 0 \,.$
Rel is the classic example of a meros, analogous to how Set is the archetypical topos.
Kawahara 1995 uses also the example of $Rel \times Rel$.
The notion of meroi was introduced in:
Last revised on October 9, 2021 at 07:32:40. See the history of this page for a list of all contributions to it.