Homotopy Type Theory SEAR > history (Rev #4)

Idea

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

Definition

A model of SEAR CC consists of

  • A type Ob(C)Ob(C), whose terms are called “sets”.

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

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

  • For each “set” A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), “relation” R:Hom(A,B)R:Hom(A,B), and “element” a:El(A)a:El(A) and b:El(B)b:El(B), a type R(a,b)R(a,b) with a term p:isProp(R(a,b))p:isProp(R(a,b))

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

    ()():Hom(B,D)×Hom(A,B)Hom(A,D)(-)\circ(-):Hom(B,D) \times Hom(A,B) \to Hom(A,D)

    and a term

    γ: A:Ob(C) B:Ob(C) D:Ob(C) R:Hom(A,B) S:Hom(B,C) a:El(A) d:El(D)(SR)(a,d)=[ b:BS(b,d)×R(a,b)]\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 [T]\left[T\right] is the propositional truncation of the type TT.

  • For each “set” A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), a relation

    id A,B:Hom(A,B)id_{A,B}:Hom(A,B)

    and terms

    p: A:Ob(C) B:Ob(C) R:Hom(A,B) a:El(A) a :El(A) b:El(B) b :El(B)(R(a,b)×id A(a,a )×id B(b,b ))R(a ,b )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 functional entire “relations” between “sets” A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) in CC be defined as

Map(A,B) f:Hom(A,B) a:El(A)isContr( b:El(B)P(f)(a,b))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)A:Ob(C) and B:Ob(C)B:Ob(C), a function ()(()):Map(A,B)×El(A)El(B)(-)((-)): Map(A,B) \times El(A) \to El(B) and a term δ:isContr(P(f)(a,f(a)))\delta:isContr(P(f)(a, f(a))).

  • A “set” A:Ob(C)A:Ob(C) with a term ϵ:[El(A)]\epsilon:\left[El(A)\right].

  • For each “set” A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and “relation” R:Hom(A,B)R:Hom(A,B), a “set” |R|:Ob(C)\vert R \vert:Ob(C) and functional entire “relation” f:Hom(|R|,A)f:Hom(\vert R \vert, A), g:Hom(|R|,B)g:Hom(\vert R \vert, B), and a term q:R=f gq:R = f^\dagger \circ g and a term

    η: x:El(|R|) y:El(|R|)(f(x)=f(y))×(g(x)=g(y))(x=y)\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:Ob(C), a “set” 𝒫(A)\mathcal{P}(A) and a “relation” A:Hom(A,𝒫(A))\in_A:Hom(A, \mathcal{P}(A)) and a term

    ι: B:Ob(C) R:Hom(A,B)[ χ R:Hom(A,P(B))isMap(χ R)×(R=( B )χ R)]\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” :Ob(C)\mathbb{N}:Ob(C) with functional entire “relations” 0:El()0:El(\mathbb{N}) and s:Hom(,)s:Hom(\mathbb{N},\mathbb{N}) and a term

κ: A:Ob(C) 0 A:El(A) s A:Hom(A,A)[ f:Hom(,A)(f(0)=0 A)× n:El()(f(s(n))=s A(f(n)))]\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)A:Ob(C) and function Q:El(A)×Ob(C)Prop 𝒰Q:El(A) \times Ob(C) \to Prop_\mathcal{U}, a “set” B:Ob(C)B:Ob(C) with a functional entire “relation” p:Hom(B,A)p:Hom(B,A), a function M:El(B)Ob(C)M:El(B) \to Ob(C) and terms
    λ: b:El(B)isContr(Q(p(b),M(b)))\lambda:\prod_{b:El(B)} isContr(Q(p(b),M(b)))
    μ: a:El(A)[ X:Ob(C)isContr(Q(a,X))][ b:Bp(b)=a]\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

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