nLab
meros

Meros

Meros

Idea

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.

Definition

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,

Definition

An I-category is a dagger category where, for all objects A,BA, B, there is a partial order \sqsubseteq on the morphisms ABA \to B, a least relation 0 A,B0_{A,B} and greatest relation Θ A,B\Theta_{A,B} such that

AB0 A,BαΘ A,B \underset{ A \to B }{ \forall } \;\; 0_{A,B} \sqsubseteq \alpha \sqsubseteq \Theta_{A,B}

and the partial order commutes with the dagger structure:

α,β:AB,αβα β . \underset{ \alpha, \beta \colon A \to B, }{ \forall } \;\; \alpha \sqsubseteq \beta \;\;\iff\;\; \alpha^\dagger \sqsubseteq \beta^\dagger \,.

I-categories can have a zero object like typical dagger categories, but also a terminal object.

Definition

When it exists, a terminal object in an I-category (Def. ) is an object 11 such that 0 1,1id 1=Θ 1,10_{1,1} \neq id_1 = \Theta_{1,1} and for all objects A,BA, B, Θ 1,BΘ A,1=Θ A,B\Theta_{1,B} \circ \Theta_{A,1} = \Theta_{A,B}.

We next highlight specific morphisms within I-categories.

Definition

A morphism f:ABf \colon A \to B in an I-category (Def. ) is called a partial function, or univalent, when ff id Bf \circ f^\dagger \sqsubseteq id_B.

Definition

A partial function f:ABf \colon A \to B (Def. ) is a total function, or function, when id Af fid_A \sqsubseteq f^\dagger \circ f.

Definition

A morphism α:AB\alpha \colon A \to B in an I-category (Def. ) is rational when there exist functions f:XAf \,\colon\, X \to A and g:XBg \,\colon\, X \to B (in the sense of Def. ) such that α=gf \alpha = g \circ f^\dagger and f fg g=id Xf^\dagger \circ f \sqcap g^\dagger \circ g = id_X.

Definition

For all α:AB,β:AC,γ:BC\alpha \,\colon\, A \to B, \beta \,\colon\, A \to C, \gamma \,\colon\, B \to C there exists a quotient β÷γ:AB\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.

(1)α:ABβ:BCγ:ACβαγ(βγα )α \underset{ { \alpha \colon A \to B } \atop { { \beta \colon B \to C } \atop { \gamma \colon A \to C } } }{ \forall } \;\; \beta \circ \alpha \sqcap \gamma \,\sqsubseteq\, ( \beta \sqcap \gamma \circ \alpha^\dagger ) \circ \alpha

We are now ready to define meroi. Instead of a lattice, we will now expect a complete Heyting algebra for each hom-set.

Definition

A meros is an I-category (Def. ) where:

  • The partial order \sqsubseteq is not just a lattice, but a complete Heyting algebra.

  • Every relation is rational (in the sense of Def. ).

  • The Dedekind formula (1) holds whenever possible.

  • There is a terminal object (in the sense of Def. ).

  • All quotients (in the sense of Def. ) exist.

Properties

Proposition

For all α,AB\alpha \,,\, A \to B we have 0α=α0=00 \circ \alpha = \alpha \circ 0 = 0.

(Kawahara 1995)
Proof

00÷αα00α0=0. 0 \sqsubseteq 0 \div \alpha \;\;\iff\;\; \alpha \circ 0 \sqsubseteq 0 \;\;\iff\;\; \alpha \circ 0 = 0 \,.

Examples

Example

Rel is the classic example of a meros, analogous to how Set is the archetypical topos.

Kawahara 1995 uses also the example of Rel×RelRel \times Rel.

References

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.