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

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

Idea

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

Definition

A model of SEAR is adagger 2-poset$C$ consists of$C$ with a set $El(A)$ of elements in $A$ for every object $A:Ob(C)$ such that

• Nontriviality: A There type exists an object$A:\mathrm{Ob}(C)$ A:Ob(C) Ob(C) , with whose a terms term are called objects.$p:\left[El(A)\right]$, where $\left[T\right]$ is the propositional truncation of the type $T$.

• Relational For comprehension: each for every object$A:Ob(C)$ , and a$B:Ob(C)$set there is a function$P:\mathrm{Hom}(A,B)\to (\mathrm{El}(A)\times \mathrm{El}(B)\to {\mathrm{Prop}}_{𝒰})$ P:Hom(A,B) El(A) \to (El(A) \times El(B) \to Prop_\mathcal{U}), whose terms are called elements.

• Function evaluation: For every each objectmap$A:Ob(C)$ and$\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; B</ins></span>}:\mathrm{<span><del\; class="diffmod">\; Hom</del><ins\; class="diffmod">\; Ob</ins></span>}(\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; C</ins></span>},B)$ f:Hom(A,B) B:Ob(C) , there is a function$(-)((-)): Hom(A,B) \times El(A) \to El(B)$set such that$\mathrm{<span><del\; class="diffmod">\; P</del><ins\; class="diffmod">\; Hom</ins></span>}(\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; A</ins></span>})(a,\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; B</ins></span>}(a))$ P(f)(a, Hom(A,B) f(a)) , is whose elements are called morphisms.contractible.

• Tabulations: For for every object$A:Ob(C)$ and $B:Ob(C)$ and there morphism is a function$\mathrm{<span><del\; class="diffmod">\; R</del><ins\; class="diffmod">\; P</ins></span>}:\mathrm{Hom}(A,B)\to (\mathrm{El}(A)\times \mathrm{El}(B)\to {\mathrm{Prop}}_{𝒰})$ R:Hom(A,B) P:Hom(A,B) \to (El(A) \times El(B) \to Prop_\mathcal{U}), 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$.

• Power For sets: for every object$A:Ob(C)$ , there is an object$\mathrm{<span><del\; class="diffmod">\; 𝒫</del><ins\; class="diffmod">\; B</ins></span>}:\mathrm{Ob}(\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; C</ins></span>})$ \mathcal{P}(A) B:Ob(C) , and a morphism${\in }_{A}C:\mathrm{<span><del\; class="diffmod">\; Hom</del><ins\; class="diffmod">\; Ob</ins></span>}(\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; C</ins></span>},𝒫(A))$ \in_A:Hom(A, C:Ob(C) \mathcal{P}(A)) such there that is for a each function morphism$R:Hom(A,B)$, there exists a map $\chi_R:Hom(A,P(B))$ such that $R = (\in_B^\dagger) \circ \chi_R$.

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

  such that

  $$\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 the type of all maps in $C$ be defined as

  $$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)$$

• Natural For numbers: each there is an object$\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; A</ins></span>}:\mathrm{Ob}(C)$ \mathbb{N}:Ob(C) A:Ob(C) with and maps$0B:\mathrm{<span><del\; class="diffmod">\; El</del><ins\; class="diffmod">\; Ob</ins></span>}(\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; C</ins></span>})$ 0:El(\mathbb{N}) B:Ob(C) , and there is a function$s(-)((-)):\mathrm{<span><del\; class="diffmod">\; Hom</del><ins\; class="diffmod">\; Map</ins></span>}(\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; A</ins></span>},\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; B</ins></span>})\times \mathrm{El}(A)\to \mathrm{El}(B)$ s:Hom(\mathbb{N},\mathbb{N}) (-)((-)): Map(A,B) \times El(A) \to El(B) , such that for every object$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; P</ins></span>}(f)(a,f(a))$ A P(f)(a, f(a)) with is maps$0_A:El(A)$contractible and $s_A:Hom(A,A)$, there is a map $f:\mathbb{N} \to A$ such that $f(0) = 0_A$ and $f \circ s = s_A \circ f$.

• Collection: There for exists every an object$A:Ob(C)$ and with function a term$\mathrm{<span><del\; class="diffmod">\; P</del><ins\; class="diffmod">\; p</ins></span>}:\mathrm{El}[\mathrm{El}(A)](A)\times \mathrm{Ob}(C)\to {\mathrm{Prop}}_{𝒰}$ P:El(A) p:\left[El(A)\right] \times Ob(C) \to Prop_\mathcal{U} , there where exists an object$B\left[T\right]:\mathrm{Ob}(C)$ B:Ob(C) \left[T\right] with is a the map propositional truncation of the type$\mathrm{<span><del\; class="diffmod">\; p</del><ins\; class="diffmod">\; T</ins></span>}:\mathrm{Hom}(A,B)$ p:Hom(A,B) T 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$.

• 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