nLab meros

Meros

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

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 11:32:40. See the history of this page for a list of all contributions to it.