Homotopy Type Theory SEAR > history (Rev #3, changes)

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

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 objects. “sets”.

• For each object “set”$A:Ob(C)$, a set $El(A)$ , whose terms are called elements. “elements”.

• For each object “set”$A:Ob(C)$ and $B:Ob(C)$, a set $Hom(A,B)$ , whose elements terms are called morphisms. “relations”.

• For every each object “set”$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})$

• For every each object “set”$A:Ob(C)$, $B:Ob(C)$, $C:Ob(C)$ , there is a function

  $$(-)\circ(-):Hom(B,C) \times Hom(A,B) \to Hom(A,C)$$

  such and that a term

  $$\gamma :\prod _{a:\mathrm{El}(A)}\prod _{c:\mathrm{El}(C)}P(R\circ S)(a,c)\iff [\sum _{b:\mathrm{El}(B)}P(R)(a,b)\times P(S)(b,c)]$$ \prod_{a:El(A)} \gamma:\prod_{a:El(A)} \prod_{c:El(C)} P(R \circ S)(a, c) \iff \left[\sum_{b:El(B)} P(R)(a,b) \times P(S)(b,c)\right]

  Let where the type of all maps in$C\left[T\right]$ C \left[T\right] be is defined the as propositional truncation of the type$T$.

  $$Map(a, b) \coloneqq \sum_{f:hom_A(a,b)} \prod_{a:El(A)} isContr\left(\sum_{b:El(B)} P(f)(a,b)\right)$$

• For each object $A:Ob(C)$ and $B:Ob(C)$, there is a function $(-)((-)): Map(A,B) \times El(A) \to El(B)$ such that $P(f)(a, f(a))$ is contractible.

• There exists an object $A:Ob(C)$ with a term $p:\left[El(A)\right]$, where $\left[T\right]$ is the propositional truncation of the type $T$.

• 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 R \vert, A)$, $g:Hom(\vert R \vert, A)$, such that $R = f^\dagger \circ g$ and for two elements $x:El(\vert R \vert)$ and $y:El(\vert R \vert)$, $f(x) = f(y)$ and $g(x) = g(y)$ imply $x = y$.

• 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 $\chi_R:Hom(A,P(B))$ such that $R = (\in_B^\dagger) \circ \chi_R$.

• There is an object $\mathbb{N}:Ob(C)$ with maps $0:El(\mathbb{N})$ and $s:Hom(\mathbb{N},\mathbb{N})$, such that for every object $A$ with maps $0_A:El(A)$ and $s_A:Hom(A,A)$, there is a map $f:Hom(\mathbb{N},A)$ such that $f(0) = 0_A$ and for all elements $n:El(\mathbb{N})$, $f(s(n)) = s_A(f(n))$.

• For every object $A:Ob(C)$ and function $P:El(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 element $b:El(B)$, $P(p(b),M(b))$ is contractible and (2) for every element $a:El(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
• Categorical SEAR