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

Showing changes from revision #3 to #4: Added | Removed | Changed

## Idea

A model of the Elementary Theory of the Category of RelationsRel (ETRel) (ETCR) is thedagger 2-poset whose category of maps is a model of ETCS?.

## Definition

A model of ETRel ETCR is adagger 2-poset $C$ such that:

• Always Singleton: true there relation: is for an every object A:Ob(C) \mathbb{1}:Ob(C) and such that for every morphism B:Ob(C) f:Hom(\mathbb{1},\mathbb{1}) , there is a morphism \top_{A,B}:Hom(A,B) f \leq 1_\mathbb{1} , such and that for every other object morphism a:Hom(A, A:Ob(C) B) , there is an$a \leq \top_{A,B}$onto dagger morphism ,$u_A:A \to \mathbb{1}$.

• Singleton: Tabulations: there for is every an object \mathbb{1}:Ob(C) A:Ob(C) such and that \top_{\mathbb{1},\mathbb{1}} B:Ob(C) = 1_\mathbb{1} , and for morphism every object A:Ob(C) R:Hom(A,B) , there is an objectonto dagger morphism$\vert R \vert:Ob(C)$ and$u_A:A \to \mathbb{1}$maps $f:Hom(\vert R \vert, A)$, $g:Hom(\vert R \vert, B)$, such that $R = f^\dagger \circ g$ and for every object $E:Ob(C)$ and maps $h:Hom(E,\vert R \vert)$ and $k:Hom(E,\vert R \vert)$, $f \circ h = f \circ k$ and $g \circ h = g \circ k$ imply $h = k$.

• Cartesian Power products: sets: for every object$A:Ob(C)$ , and there is an object B:Ob(C) \mathcal{P}(A) and a morphism R:Hom(A,B) \in_A:Hom(A, \mathcal{P}(A)) , there such is that an for object each morphism A R:Hom(A,B) \times B:Ob(C) , and there exists a maps map  f:Hom(A \chi_R:Hom(A,P(B)) \times B, A) , such that g:Hom(A R \times = B, (\in_B^\dagger) B) \circ \chi_R, such that $\top_{A,B} = f^\dagger \circ g$.

• Tabulations: Function extensionality: 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 maps  f:Hom(\vert f:Hom(A, R B) \vert, A),  g:Hom(\vert g:Hom(A, R B) \vert, A) , such and that R x:Hom(\mathbb{1}, = A) f^\dagger \circ g , and for two global elements x:Hom(\mathbb{1},\vert f R \circ \vert) x = g \circ x and implies y:Hom(\mathbb{1},\vert f R = \vert) g, $f \circ x = f \circ y$ and $g \circ x = g \circ y$ imply $x = y$.

• Power Natural sets: numbers: for there every is an object A:Ob(C) \mathbb{N}:Ob(C) , there with is maps an object \mathcal{P}(A) 0:\mathbb{1} \to \mathbb{N} and a morphism \in_A:Hom(A, s:\mathbb{N} \mathcal{P}(A)) \to \mathbb{N} , such that for each morphism object R:Hom(A,B) A , there with exists maps amap$0_A:\mathbb{1} \to A$ and \chi_R:Hom(A,P(B)) s_A:A \to A , such there that is a map R f:\mathbb{N} = \to (\in_B^\dagger) A \circ \chi_R such that $f \circ 0 = 0_A$ and $f \circ s = s_A \circ f$.

• Function Choice: extensionality: for every object$A:Ob(C)$ and $B:Ob(C)$ , and every maps entire $f:Hom(A, B)$dagger epimorphism , g:Hom(A, R: B) Hom(A,B) and has a section.$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: Hom(A,B)$ has a section.