nLab ETCR

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 CC such that:

  • Singleton: there is an object 𝟙Ob(C)\mathbb{1} \in Ob(C) such that for every morphism fHom(𝟙,𝟙)f \in Hom(\mathbb{1},\mathbb{1}), f1 𝟙f \leq 1_\mathbb{1}, and for every object AOb(C)A \in Ob(C) there is an onto morphism u AHom(A,𝟙)u_A \in Hom(A,\mathbb{1}).

  • Tabulations: for every object AOb(C)A \in Ob(C) and BOb(C)B \in Ob(C) and morphism RHom(A,B)R \in Hom(A,B), there is an object |R|Ob(C)\vert R \vert \in Ob(C) and jointly monic maps fHom(|R|,A)f \in Hom(\vert R \vert, A), gHom(|R|,B)g \in Hom(\vert R \vert, B), such that R=f gR = f^\dagger \circ g.

  • Power sets: for every object AOb(C)A \in Ob(C), there is an object 𝒫(A)\mathcal{P}(A) and a morphism A:Hom(A,𝒫(A))\in_A:Hom(A, \mathcal{P}(A)) such that for each morphism RHom(A,B)R \in Hom(A,B), there exists a map χ RHom(A,P(B))\chi_R \in Hom(A,P(B)) such that R=( B )χ RR = (\in_B^\dagger) \circ \chi_R.

  • Function extensionality: for every object AOb(C)A \in Ob(C) and BOb(C)B \in Ob(C) and maps fHom(A,B)f \in Hom(A, B), gHom(A,B)g \in Hom(A, B) and xHom(𝟙,A)x \in Hom(\mathbb{1}, A), fx=gxf \circ x = g \circ x implies f=gf = g.

  • Natural numbers: there is an object Ob(C)\mathbb{N} \in Ob(C) with maps 0Hom(𝟙,)0 \in Hom(\mathbb{1},\mathbb{N}) and sHom(,)s \in Hom(\mathbb{N},\mathbb{N}), such that for each object AA with maps 0 AHom(𝟙,A)0_A \in Hom(\mathbb{1},A) and s AHom(A,A)s_A \in Hom(A,A), there is a map fHom(,A)f \in Hom(\mathbb{N},A) such that f0=0 Af \circ 0 = 0_A and fs=s Aff \circ s = s_A \circ f.

  • Choice: for every object AOb(C)A \in Ob(C) and BOb(C)B \in Ob(C), every epic map RHom(A,B)R \in Hom(A,B) has a section.

See also

Last revised on May 13, 2022 at 20:37:48. See the history of this page for a list of all contributions to it.