## Idea A model of the **Elementary Theory of the Category of Relations** (ETCR) is the [[dagger 2-poset]] whose [[category of maps]] is a model of [[ETCS]]. ## Definition A model of ETCR is a [[dagger 2-poset]] $C$ such that: * Singleton: there is an object $\mathbb{1}:Ob(C)$ such that for every morphism $f:Hom(\mathbb{1},\mathbb{1})$, $f \leq 1_\mathbb{1}$, and for every object $A:Ob(C)$ there is an [[onto dagger morphism in a dagger 2-poset|onto dagger morphism]] $u_A:A \to \mathbb{1}$. * Tabulations: for every object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A,B)$, there is an object $\vert R \vert:Ob(C)$ and [[map in a dagger 2-poset|maps]] $f:Hom(\vert R \vert, A)$, $g:Hom(\vert R \vert, B)$, such that $R = f^\dagger \circ g$ and for every object $E:Ob(C)$ and maps $h:Hom(E,\vert R \vert)$ and $k:Hom(E,\vert R \vert)$, $f \circ h = f \circ k$ and $g \circ h = g \circ k$ imply $h = k$. * Power sets: for every object $A:Ob(C)$, there is an object $\mathcal{P}(A)$ and a morphism $\in_A:Hom(A, \mathcal{P}(A))$ such that for each morphism $R:Hom(A,B)$, there exists a [[map in a dagger 2-poset|map]] $\chi_R:Hom(A,P(B))$ such that $R = (\in_B^\dagger) \circ \chi_R$. * Function extensionality: for every object $A:Ob(C)$ and $B:Ob(C)$ and [[map in a dagger 2-poset|maps]] $f:Hom(A, B)$, $g:Hom(A, B)$ and $x:Hom(\mathbb{1}, A)$, $f \circ x = g \circ x$ implies $f = g$. * Natural numbers: there is an object $\mathbb{N}:Ob(C)$ with maps $0:\mathbb{1} \to \mathbb{N}$ and $s:\mathbb{N} \to \mathbb{N}$, such that for each object $A$ with maps $0_A:\mathbb{1} \to A$ and $s_A:A \to A$, there is a map $f:\mathbb{N} \to A$ such that $f \circ 0 = 0_A$ and $f \circ s = s_A \circ f$. * Choice: for every object $A:Ob(C)$ and $B:Ob(C)$, every [[entire dagger morphism in a dagger 2-poset|entire]] [[dagger epimorphism in a dagger precategory|dagger epimorphism]] $R: Hom(A,B)$ has a section. ## See also * [[Rel]] * [[ETCS]] * [[Categorical SEAR]] * [[SEAR]]