## Idea A general (non-concrete) categorical version of [[Mike Shulman]]'s dependently typed first-order theory [[SEAR]]. ## Definition Assuming excluded middle, a model of categorical SEAR is a [[dagger 2-poset]] $C$ such that: * Singleton: there is an object $\mathbb{1}:Ob(C)$ such that for every other morphism $a:Hom(\mathbb{1}, \mathbb{1})$, $a \leq 1_\mathbb{1}$, and for every object $A:Ob(C)$ there is an [[onto dagger morphism in a dagger 2-poset|onto dagger morphism]] $u_A:A \to \mathbb{1}$. * Function extensionality: for every object $A:Ob(C)$ and $B:Ob(C)$, [[map in a dagger 2-poset|maps]] $f:Hom(A, B)$ and $g:Hom(A, B)$, and global element $x:Hom(\mathbb{1}, A)$, $f \circ x = g \circ x$ implies $f = g$. * Relational comprehension: for every object $A:Ob(C)$ and $B:Ob(C)$ there is a function $P:Hom(A,B) \to (El(A) \times El(B) \to Prop_\mathcal{U})$ * 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 [[map in a dagger 2-poset|maps]] $f:Hom(\vert R \vert, A)$, $g:Hom(\vert R \vert, A)$, such that $R = f^\dagger \circ g$ 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 in a dagger 2-poset|map]] $\chi_R:Hom(A,P(B))$ such that $R = (\in_B^\dagger) \circ \chi_R$. * Natural numbers: there is an object $\mathbb{N}:Ob(C)$ with maps $0:Hom(\mathbb{1},\mathbb{N})$ and $s:Hom(\mathbb{N},\mathbb{N})$, such that for every object $A$ with maps $0_A:Hom(\mathbb{1},A)$ and $s_A:Hom(A,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$. * Collection: for every object $A:Ob(C)$ and function $P:Hom(\mathbb{1},A) \times Ob(C) \to Prop_\mathcal{U}$, there exists an object $B:Ob(C)$ with a map $p:Hom(A,B)$ and a $B$-indexed family of objects $M:Hom(\mathbb{1},B) \to \mathcal{U}$ such that (1) for every global element $b:Hom(\mathbb{1},B)$, $P(p(b),M(b))$ is [[contractible]] and (2) for every global element $a:Hom(\mathbb{1},A)$, if there exists an object $X:Ob(C)$ such that $P(a,X)$ is [[contractible]], then $a$ is in the image of $p$. ## See also * [[Rel]] * [[SEAR]]