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

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

Idea

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

Definition

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

• Always true relation: for every object$A:Ob(C)$ and $B:Ob(C)$ , there is a morphism${\top }_{A,B}:\mathrm{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 \leq \top_{A,B}$,

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

• Cartesian products: for every object$A:Ob(C)$ and $B:Ob(C)$ , an and object morphism$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; R</ins></span>}\otimes B:\mathrm{<span><del\; class="diffmod">\; Ob</del><ins\; class="diffmod">\; Hom</ins></span>}(\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; A</ins></span>},B)$ A R:Hom(A,B) \otimes B:Ob(C) , and there is an object$A \times B:Ob(C)$ and maps $p_{A}f:\mathrm{Hom}(A<span><del\; class="diffmod">\; \otimes </del><ins\; class="diffmod">\; \times </ins></span>B<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; ,</ins></span>A)$ p_A:A f:Hom(A \otimes \times B B, \to A) A , and$p_{B}g:\mathrm{Hom}(A\times B<span><del\; class="diffmod">\; \otimes </del><ins\; class="diffmod">\; ,</ins></span>B<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; )</ins></span>B$ p_B:B g:Hom(A \otimes \times B B, \to B) B , such that$p_B^{†}\circ p_A={\top }_{A,B}=f^{†}\circ g$ p_B^\dagger \circ p_A = \top_{A,B} = f^\dagger \circ g and $u_B \circ p_B = u_A \circ p_A$ for every onto dagger morphism $u_A:A \to \mathbb{1}$ and $u_B: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 functional maps dagger monomorphism$f:Hom(\vert R \vert, A)$ ,$\mathrm{<span><del\; class="diffmod">\; i</del><ins\; class="diffmod">\; g</ins></span>}:\mathrm{Hom}(|R|,A\otimes B)$ i:Hom(\vert g:Hom(\vert R \vert, A A) \otimes B), such that $R=(f^{†}{p}_b\circ \mathrm{<span><del\; class="diffmod">\; i</del><ins\; class="diffmod">\; g</ins></span>}{)}^{†}\circ (p_A\circ i)$ R = (p_b f^\dagger \circ i)^\dagger g \circ (p_A \circ i) and for two global elements $x:Hom(\mathbb{1},\vert R \vert)$ and $y:Hom(\mathbb{1},\vert R \vert)$, $f \circ x = f \circ y$ and $g \circ x = g \circ y$ imply $x = y$.

• 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 $\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 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 epimorphism $R:\mathrm{Hom}(A<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; ,</ins></span>B)$ R: A Hom(A,B) \to B has a section.

See also

• Rel
• ETCS?
• Categorical SEAR