## Idea [[Mike Shulman]]'s dependently typed first-order theory SEAR. ## Definition A model of SEAR $C$ consists of * A type $Ob(C)$, whose terms are called "sets". * For each "set" $A:Ob(C)$, a [[set]] $El(A)$, whose terms are called "elements". * For each "set" $A:Ob(C)$ and $B:Ob(C)$, a [[set]] $Hom(A,B)$, whose terms are called "relations". * For each "set" $A:Ob(C)$ and $B:Ob(C)$, "relation" $R:Hom(A,B)$, and "element" $a:El(A)$ and $b:El(B)$, a type $R(a,b)$ with a term $p:isProp(R(a,b))$ * For each "set" $A:Ob(C)$, $B:Ob(C)$, $D:Ob(C)$, a function $$(-)\circ(-):Hom(B,D) \times Hom(A,B) \to Hom(A,D)$$ and a term $$\gamma:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Hom(A,B)} \prod_{S:Hom(B,C)} \prod_{a:El(A)} \prod_{d:El(D)} (S \circ R)(a, d) = \left[\sum_{b:B} S(b,d) \times R(a,b)\right]$$ where $\left[T\right]$ is the propositional truncation of the type $T$. * For each "set" $A:Ob(C)$, $B:Ob(C)$, a relation $$id_{A,B}:Hom(A,B)$$ and terms $$p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \prod_{a:El(A)} \prod_{a^{'}:El(A)} \prod_{b:El(B)} \prod_{b^{'}:El(B)} (R(a,b) \times id_A(a,a^{'}) \times id_B(b,b^{'})) \to R(a^{'},b^{'})$$ Let the type of all [[map in a dagger 2-poset|functional entire]] "relations" between "sets" $A:Ob(C)$ and $B:Ob(C)$ in $C$ be defined as $$Map(A, B) \coloneqq \sum_{f:Hom(A,B)} \prod_{a:El(A)} isContr\left(\sum_{b:El(B)} P(f)(a,b)\right)$$ * For each "set" $A:Ob(C)$ and $B:Ob(C)$, a function $(-)((-)): Map(A,B) \times El(A) \to El(B)$ and a term $\delta:isContr(P(f)(a, f(a)))$. * A "set" $A:Ob(C)$ with a term $\epsilon:\left[El(A)\right]$. * For each "set" $A:Ob(C)$ and $B:Ob(C)$ and "relation" $R:Hom(A,B)$, a "set" $\vert R \vert:Ob(C)$ and functional entire "relation" $f:Hom(\vert R \vert, A)$, $g:Hom(\vert R \vert, B)$, and a term $q:R = f^\dagger \circ g$ and a term $$\eta:\prod_{x:El(\vert R \vert)} \prod_{y:El(\vert R \vert)} (f(x) = f(y)) \times (g(x) = g(y)) \to (x = y)$$ * For each "set" $A:Ob(C)$, a "set" $\mathcal{P}(A)$ and a "relation" $\in_A:Hom(A, \mathcal{P}(A))$ and a term $$\iota:\prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \left[\sum_{\chi_R:Hom(A,P(B))} isMap(\chi_R) \times (R = (\in_B^\dagger) \circ \chi_R)\right]$$ * A "set" $\mathbb{N}:Ob(C)$ with functional entire "relations" $0:El(\mathbb{N})$ and $s:Hom(\mathbb{N},\mathbb{N})$ and a term $$\kappa:\prod_{A:Ob(C)} \prod_{0_A:El(A)} \prod_{s_A:Hom(A,A)} \left[\sum_{f:Hom(\mathbb{N},A)} (f(0) = 0_A) \times \prod_{n:El(\mathbb{N})} (f(s(n)) = s_A(f(n)))\right]$$ * For each "set" $A:Ob(C)$ and function $Q:El(A) \times Ob(C) \to Prop_\mathcal{U}$, a "set" $B:Ob(C)$ with a functional entire "relation" $p:Hom(B,A)$, a function $M:El(B) \to Ob(C)$ and terms $$\lambda:\prod_{b:El(B)} isContr(Q(p(b),M(b)))$$ $$\mu:\prod_{a:El(A)} \left[\sum_{X:Ob(C)} isContr(Q(a,X))\right] \to \left[\sum_{b:B} p(b) = a\right]$$ ## See also * [[Rel]] * [[Categorical SEAR]] * [[SEPS]] * [[ZF]]