Homotopy Type Theory ETCR > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


A model of the Elementary Theory of Rel (ETRel) is the dagger 2-poset whose category of maps is a model of ETCS?.


A model of ETRel is a dagger 2-poset CC with: such that:

  • Always true relation: for every objectA:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) , there is a morphism A,B:Hom(A,B) \top_{A,B}:Hom(A, \top_{A,B}:Hom(A,B) B) such that for every other morphism a:Hom(A,B)a:Hom(A, B), a A,Ba \leq \top_{A,B},

  • Singleton: there is an object𝟙:Ob(C)\mathbb{1}:Ob(C) such that 𝟙,𝟙=1 𝟙\top_{\mathbb{1},\mathbb{1}} = 1_\mathbb{1}, and for every object A:Ob(C)A:Ob(C) , there is anonto dagger morphism u A:A𝟙u_A:A \to \mathbb{1}.

  • Cartesian products: for every objectA:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) , an and object morphism A RB: Ob Hom( C A,B) A R:Hom(A,B) \otimes B:Ob(C) , and there is an objectA×B:Ob(C)A \times B:Ob(C) and maps p Af:Hom(A ×B ,A) p_A:A f:Hom(A \otimes \times B B, \to A) A , andp Bg:Hom(A×B ,B )B p_B:B g:Hom(A \otimes \times B B, \to B) B , such thatp B p A= A,B=f g p_B^\dagger \circ p_A = \top_{A,B} = f^\dagger \circ g and u Bp B=u Ap Au_B \circ p_B = u_A \circ p_A for every onto dagger morphism u A:A𝟙u_A:A \to \mathbb{1} and u B:A𝟙u_B:A \to \mathbb{1}.

  • Tabulations: for every objectA: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 functional maps dagger monomorphismf:Hom(|R|,A)f:Hom(\vert R \vert, A) , i g:Hom(|R|,AB) i:Hom(\vert g:Hom(\vert R \vert, A A) \otimes B), such that R=(f p b i g) (p Ai) R = (p_b f^\dagger \circ i)^\dagger g \circ (p_A \circ i) and for two global elements x:Hom(𝟙,|R|)x:Hom(\mathbb{1},\vert R \vert) and y:Hom(𝟙,|R|)y:Hom(\mathbb{1},\vert R \vert), fx=fyf \circ x = f \circ y and gx=gyg \circ x = g \circ y imply x=yx = y.

  • Power sets: for every objectA: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 objectA: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 objectA:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), every entire dagger epimorphism R:Hom(A ,B) R: A Hom(A,B) \to B has a section.

See also

Revision on April 20, 2022 at 14:42:28 by Anonymous?. See the history of this page for a list of all contributions to it.