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 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 A×BA \times B, whose terms are called “pairs”.

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

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

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

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

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

    and a term

    γ: A:Ob(C) B:Ob(C) D:Ob(C) R:Sub(A×B) S:Sub(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: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 [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:Sub(A×B)id_{A,B}:Sub(A \times B)

    and terms

    p: A:Ob(C) B:Ob(C) R:Sub(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: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)A:Ob(C) and B:Ob(C)B:Ob(C) in CC be defined as

Map(A,B) f:Sub(A×B) a:El(A)isContr( b:El(B)P(f)(a,b))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)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), there is a function |()|:Sub(A)Ob(C)\vert(-)\vert:Sub(A) \to Ob(C), and for every subset S:Sub(A)S:Sub(A) there is an injection? i:|S|Ai:\vert S \vert \to A.

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

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

κ: A:Ob(C) 0 A:El(A) s A:Sub(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: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)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:Sub(B×A)p:Sub(B \times 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 June 7, 2022 at 22:18:35 by Anonymous?. See the history of this page for a list of all contributions to it.