Homotopy Type Theory ETCR > history (Rev #4)

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}:Ob(C) such that for every morphism f:Hom(𝟙,𝟙)f:Hom(\mathbb{1},\mathbb{1}), f1 𝟙f \leq 1_\mathbb{1}, and for every object A:Ob(C)A:Ob(C) there is an onto dagger morphism u A:A𝟙u_A:A \to \mathbb{1}.

  • Tabulations: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and morphism R:Hom(A,B)R:Hom(A,B), there is an object |R|:Ob(C)\vert R \vert:Ob(C) and maps f:Hom(|R|,A)f:Hom(\vert R \vert, A), g:Hom(|R|,B)g:Hom(\vert R \vert, B), such that R=f gR = f^\dagger \circ g and for every object E:Ob(C)E:Ob(C) and maps h:Hom(E,|R|)h:Hom(E,\vert R \vert) and k:Hom(E,|R|)k:Hom(E,\vert R \vert), fh=fkf \circ h = f \circ k and gh=gkg \circ h = g \circ k imply h=kh = k.

  • Power sets: for every object A:Ob(C)A: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 R:Hom(A,B)R:Hom(A,B), there exists a map χ R:Hom(A,P(B))\chi_R:Hom(A,P(B)) such that R=( B )χ RR = (\in_B^\dagger) \circ \chi_R.

  • Function extensionality: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and maps f:Hom(A,B)f:Hom(A, B), g:Hom(A,B)g:Hom(A, B) and x:Hom(𝟙,A)x: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}:Ob(C) with maps 0:𝟙0:\mathbb{1} \to \mathbb{N} and s:s:\mathbb{N} \to \mathbb{N}, such that for each object AA with maps 0 A:𝟙A0_A:\mathbb{1} \to A and s A:AAs_A:A \to A, there is a map f:Af:\mathbb{N} \to A such that f0=0 Af \circ 0 = 0_A and fs=s Aff \circ s = s_A \circ f.

  • Choice: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), every entire dagger epimorphism R:Hom(A,B)R: Hom(A,B) has a section.

See also

Revision on April 23, 2022 at 03:49:54 by Anonymous?. See the history of this page for a list of all contributions to it.