Homotopy Type Theory ETCR > history (Rev #1)

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:

for every object $A:Ob(C)$ and $B:Ob(C)$ , a morphism $\top_{A,B}:Hom(A, B)$ such that for every other morphism $a:Hom(A, B)$ , $a \leq \top_{A,B}$
an object $\mathbb{1}:Ob(C)$ such that $\top_{\mathbb{1},\mathbb{1}} = 1_\mathbb{1}$ , and for every object $A:Ob(C)$ , an onto dagger morphism $u_A:A \to \mathbb{1}$ .
for every object $A:Ob(C)$ and $B:Ob(C)$ , an object $A \otimes B:Ob(C)$ and maps $p_A:A \otimes B \to A$ and $p_B:B \otimes B \to B$ such that $p_B^\dagger \circ p_A = \top_{A,B}$ 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}$ .
for every object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A,B)$ , an object $\vert R \vert:Ob(C)$ and functional dagger monomorphism $i:Hom(\vert R \vert, A \otimes B)$ , such that $R = (p_b \circ i)^\dagger \circ (p_A \circ i)$ .
for every object $A:Ob(C)$ , 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$ .
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$ .
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$ .
for every object $A:Ob(C)$ and $B:Ob(C)$ , every entire dagger epimorphism $R: A \to B$ has a section.

Homotopy Type Theory ETCR > history (Rev #1)

Idea

Definition

See also