Homotopy Type Theory Categorical SEAR > history (Rev #3)

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 CC such that:

  • Singleton: there is an object 𝟙:Ob(C)\mathbb{1}:Ob(C) such that for every other morphism a:Hom(𝟙,𝟙)a:Hom(\mathbb{1}, \mathbb{1}), a1 𝟙a \leq 1_\mathbb{1}, and for every object A:Ob(C)A:Ob(C) there is an onto dagger morphism u A:A𝟙u_A:A \to \mathbb{1}.

  • Function extensionality: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), maps f:Hom(A,B)f:Hom(A, B) and g:Hom(A,B)g:Hom(A, B), and global element x:Hom(𝟙,A)x:Hom(\mathbb{1}, A), fx=gxf \circ x = g \circ x implies f=gf = g.

  • Relational comprehension: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) there is a function P:Hom(A,B)(El(A)×El(B)Prop 𝒰)P:Hom(A,B) \to (El(A) \times El(B) \to Prop_\mathcal{U})

  • Tabulations: for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and morphism R:Hom(A,B)R:Hom(A,B), there is an object |R|:Ob(C)\vert R \vert:Ob(C) and maps f:Hom(|R|,A)f:Hom(\vert R \vert, A), g:Hom(|R|,A)g:Hom(\vert R \vert, A), such that R=f gR = f^\dagger \circ g and for two global elements x:Hom(𝟙,|R|)x:Hom(\mathbb{1},\vert R \vert) and y:Hom(𝟙,|R|)y:Hom(\mathbb{1},\vert R \vert), fx=fyf \circ x = f \circ y and gx=gyg \circ x = g \circ y imply x=yx = y.

  • Power sets: for every object A:Ob(C)A:Ob(C), there is an object 𝒫(A)\mathcal{P}(A) and a morphism A:Hom(A,𝒫(A))\in_A:Hom(A, \mathcal{P}(A)) such that for each morphism R:Hom(A,B)R:Hom(A,B), there exists a map χ R:Hom(A,P(B))\chi_R:Hom(A,P(B)) such that R=( B )χ RR = (\in_B^\dagger) \circ \chi_R.

  • Natural numbers: there is an object :Ob(C)\mathbb{N}:Ob(C) with maps 0:Hom(𝟙,)0:Hom(\mathbb{1},\mathbb{N}) and s:Hom(,)s:Hom(\mathbb{N},\mathbb{N}), such that for every object AA with maps 0 A:Hom(𝟙,A)0_A:Hom(\mathbb{1},A) and s A:Hom(A,A)s_A:Hom(A,A), there is a map f:Af:\mathbb{N} \to A such that f0=0 Af \circ 0 = 0_A and fs=s Aff \circ s = s_A \circ f.

  • Collection: for every object A:Ob(C)A:Ob(C) and function P:Hom(𝟙,A)×Ob(C)Prop 𝒰P:Hom(\mathbb{1},A) \times Ob(C) \to Prop_\mathcal{U}, there exists an object B:Ob(C)B:Ob(C) with a map p:Hom(A,B)p:Hom(A,B) and a BB-indexed family of objects M:Hom(𝟙,B)𝒰M:Hom(\mathbb{1},B) \to \mathcal{U} such that (1) for every global element b:Hom(𝟙,B)b:Hom(\mathbb{1},B), P(p(b),M(b))P(p(b),M(b)) is contractible and (2) for every global element a:Hom(𝟙,A)a:Hom(\mathbb{1},A), if there exists an object X:Ob(C)X:Ob(C) such that P(a,X)P(a,X) is contractible, then aa is in the image of pp.

See also

Revision on April 20, 2022 at 17:20:30 by Anonymous?. See the history of this page for a list of all contributions to it.