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

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

## Idea

< SEPS

Mike Shulman’s dependently typed first-order theory SEPS.

## Definition

A model of SEPS $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 $A \times B$, whose terms are called “pairs”.

• For each “set” $A:Ob(C)$ and $B:Ob(C)$, a function $((-),(-)):El(A) \times El(B) \to El(A \times B)$ with functions $p_A:El(A \times B) \to El(A)$ and $p_B:El(A \times B) \to El(B)$

• For each “set” $A:Ob(C)$, a type $Sub(A)$, whose terms are called “subsets”, and a term $p:isHeytAlg(Sub(A))$

A “relation” is a term $R:Sub(A \times B)$.

• For each “set” $A:Ob(C)$, $B:Ob(C)$, $D:Ob(C)$, a function

$(-)\circ(-):Sub(B \times D) \times Sub(A \times B) \to Sub(A \times D)$

and a term

$\gamma:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Sub(A \times B)} \prod_{S:Sub(B \times 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}:Sub(A \times B)$

and terms

$p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Sub(A \times 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 functional entire “relations” between “sets” $A:Ob(C)$ and $B:Ob(C)$ in $C$ be defined as

$Map(A, B) \coloneqq \sum_{f:Sub(A \times 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)$, there is a function $\vert(-)\vert:Sub(A) \to Ob(C)$, and for every subset $S:Sub(A)$ there is an injection? $i:\vert S \vert \to A$.

• For each “set” $A:Ob(C)$, a “set” $\mathcal{P}(A)$ and a “relation” $\in_A:Sub(A \times \mathcal{P}(A))$ and a term

$\iota:\prod_{B:Ob(C)} \prod_{R:Sub(A \times 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:Sub(\mathbb{N} \times \mathbb{N})$ and a term

$\kappa:\prod_{A:Ob(C)} \prod_{0_A:El(A)} \prod_{s_A:Sub(A \times 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:Sub(B \times 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]$