Homotopy Type Theory ETCS as a dependent type theory > history (Rev #2, changes)

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

\tableofcontents <ETCS

\section{Idea}

There is a relation between category theory and dependent type theory which states that the internal logic? or syntax? of any category is a dependent type theory and the semantics of any dependent type theory is a category. In particular, this means that every model of ETCS?, or every well-pointed topos? with a natural numbers object? and whose epimorphisms are split, has an associated dependent type theory.

In this article, we present a model of dependent type theory whose types behave as the objects of ETCS do, and whose terms behave as the global elements of ETCS do.

\section{Presentation}

The dependent type theory we shall be presenting here is similar to objective type theory? of Benno van den Berg and Martijn den Besten?, in that it doesn’t have definitional equality. The lack of definitional equality means that the theory is both simpler, and behaves more like traditional formulations of ETCS?, which usually also doesn’t have definitional equality.

\subsection{Judgments and contexts}

The dependent type theory model of ETCS consists of three judgments: set judgments AsetA \; \mathrm{set}, where we judge AA to be a set, membership judgments, where we judge aa to be an element of AA, aAa \in A, and context judgments, where we judge Γ\Gamma to be a context, Γctx\Gamma \; \mathrm{ctx}. Contexts are lists of membership judgments aAa \in A, bBb \in B, cCc \in C, et cetera, and are formalized by the rules for the empty context and extending the context by a membership judgment

()ctxΓctxΓAset(Γ,aA)ctx\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{set}}{(\Gamma, a \in A) \; \mathrm{ctx}}

\subsection{Structural rules}

The structural rules of this theory include the variable rule?, the weakening rule?, and the substitution rule?.

The variable rule states that we may derive a membership judgment if the membership judgment is in the context already:

Γ,aA,ΔctxΓ,aA,ΔaA\frac{\vdash \Gamma, a \in A, \Delta \; \mathrm{ctx}}{\vdash \Gamma, a \in A, \Delta \vdash a \in A}

Let 𝒥\mathcal{J} be any arbitrary judgment. Then we have the following rules:

The weakening rule:

Γ,Δ𝒥ΓAsetΓ,aA,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A, \Delta \vdash \mathcal{J}}

The substitution rule:

ΓaAΓ,binA,Δ𝒥Γ,Δ[a/b]𝒥[a/b]\frac{\Gamma \vdash a \in A \quad \Gamma, b in A, \Delta \vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}

The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.

\subsection{Indexed sets and indexed elements}

An indexed set is a set BB in the context of the variable judgment xAx \in A, xABsetx \in A \vdash B \; \mathrm{set}, they are usually written as B(x)B(x) to indicate its dependence upon xx.

An indexed element is an element bBb \in B in the context of the variable judgment xAx \in A, xAbBx \in A \vdash b \in B. Sections are likewise usually written as b(x)b(x) to indicate its dependence upon xx.

\subsection{Equality}

Equality of elements of a set is represented by a set. This in other dependent type theories? is called a identity type or a path type. Equality of proofs comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:

Formation rule for equality of elements:

ΓAsetΓ,aA,bAa= Abset\frac{\Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A, b \in A \vdash a =_A b \; \mathrm{set}}

Introduction rule for equality of elements:

ΓAsetΓ,aArefl A(a)a= Aa\frac{\Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A \vdash \mathrm{refl}_A(a) \in a =_A a}

Elimination rule for equality of elements:

Γ,aA,bA,pa= Ab,Δ(a,b,p)C(a,b,p)setΓ,aA,Δ(a,a,refl A(a))tC(a,a,refl A(a))Γ,aA,bA,pa= Ab,Δ(a,b,p)J(t,a,b,p)C(a,b,p)\frac{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{set} \quad \Gamma, a \in A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t \in C(a, a, \mathrm{refl}_A(a))}{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash J(t, a, b, p) \in C(a, b, p)}

Computation rules for equality of elements:

Γ,aA,bA,pa= Ab,Δ(a,b,p)C(a,b,p)setΓ,aA,Δ(a,a,refl A(a))tC(a,a,refl A(a))Γ,aA,bA,pa= Ab,Δ(a,b,p)β = A(a)J(t,a,a,refl(a))= C(a,a,refl A(a))t\frac{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{set} \quad \Gamma, a \in A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t \in C(a, a, \mathrm{refl}_A(a))}{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) \in J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}

Uniqueness rules for equality of elements:

ΓAsetΓaAΓpa= AaΓK(a,p)p= a= Aarefl A(a)\frac{\Gamma\vdash A \; \mathrm{set} \quad \Gamma \vdash a \in A \quad \Gamma \vdash p \in a =_A a}{\Gamma\vdash K(a, p) \in p =_{a =_A a} refl_A(a)}

\subsection{Definitions of elements}

Parts of the following section is adapted from Egbert Rijke’s Introduction to Homotopy Type Theory?:

We can make definitions at the end of a derivation if the conclusion is a certain element of a set in context, where we have a derivation

𝒟ΓaA\frac{\mathcal{D}}{\Gamma \vdash a \in A}

if we wish to make a definition bab \coloneqq a, then we can extend the derivation tree with

ΓaAΓbaA\frac{\Gamma \vdash a \in A}{\Gamma \vdash b \coloneqq a \in A}

The effect of such a definition is that we have extended our type theory with a new constant bb, for which the following inference rules are valid

𝒟bA𝒟defeq(a,b)b= Aa\frac{\mathcal{D}}{b \in A} \qquad \frac{\mathcal{D}}{\mathrm{defeq}(a, b) \in b =_A a}

\subsection{Function sets}

Formation rules for function sets:

ΓAsetΓBsetΓB Aset\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma \vdash B \; \mathrm{set}}{\Gamma \vdash B^A \; \mathrm{set}}

Introduction rules for function sets:

Γ,xAb(x)BΓ(xb(x))B A\frac{\Gamma, x \in A \vdash b(x) \in B}{\Gamma \vdash (x \mapsto b(x)) \in B^A}

Elimination rules for function sets:

ΓfB AΓaAΓf(a)B\frac{\Gamma \vdash f \in B^A \quad \Gamma \vdash a \in A}{\Gamma \vdash f(a) \in B}

Computation rules for function sets:

Γ,xAb(x)BΓaAΓβ func(xb(x))(a)= Bb\frac{\Gamma, x \in A \vdash b(x) \in B \quad \Gamma \vdash a \in A}{\Gamma \vdash \beta_{\mathrm{func}} \in (x \mapsto b(x))(a) =_{B} b}

Uniqueness rules for function sets:

ΓfB AΓη funcf= B A(xf(x))\frac{\Gamma \vdash f \in B^A}{\Gamma \vdash \eta_{\mathrm{func}} \in f =_{B^A} (x \to f(x))}

\subsection{Indexed product sets}

Formation rules for Pi types:

ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}

Introduction rules for Pi types:

Γ,x:Ab(x):B(x)Γλ(x:A).b(x): x:AB(x)\frac{\Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}

Elimination rules for Pi types:

Γf:x:AB(x)Γa:AΓf(a):B[a/x]\frac{\Gamma \vdash f:\prod{x:A} B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}

Computation rules for Pi types:

Γ,x:Ab(x):B(x)Γa:AΓβ Π:λ(x:A).b(x)(a)= B[a/x]b[a/x]\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\Pi:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}

Uniqueness rules for Pi types:

Γf: x:AB(x)Γη Π:f= x:AB(x)λ(x).f(x)\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash \eta_\Pi:f =_{\prod_{x:A} B(x)} \lambda(x).f(x)}

\subsection{Product types}

We use the negative presentation for product types.

Formation rules for product types:

ΓAtypeΓBtypeΓA×Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}

Introduction rules for product types:

Γa:AΓb:BΓ(a,b):A×B\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash (a, b):A \times B}

Elimination rules for product types:

Γz:A×BΓπ 1(z):AΓz:A×BΓπ 2(z):B\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_2(z):B}

Computation rules for product types:

Γa:AΓb:BΓβ ×1:π 1(a,b)= AaΓa:AΓb:BΓβ ×2:π 2(a,b)= Bb\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 2}:\pi_2(a, b) =_B b}

Uniqueness rules for product types:

Γz:A×BΓη ×:z= A×B(π 1(z),π 2(z))\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \eta_\times:z =_{A \times B} (\pi_1(z), \pi_2(z))}

\subsection{Sigma types}

We use the negative presentation for sigma types.

Formation rules for Sigma types:

ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}

Introduction rules for Sigma types:

Γ,x:Ab(x):B(x)Γa:AΓb:B[a/x]Γ(a,b): x:AB(x)\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash (a, b):\sum_{x:A} B(x)}

Elimination rules for Sigma types:

Γz: x:AB(x)Γπ 1(z):AΓz: x:AB(x)Γπ 2(z):B(π 1(z))\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_2(z):B(\pi_1(z))}

Computation rules for Sigma types:

Γ,x:Ab(x):B(x)Γa:AΓβ Σ1:π 1(a,b)= AaΓ,x:Ab:BΓa:AΓβ Σ2:π 2(a,b)= Bπ 1(a,b)b\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 2}:\pi_2(a, b) =_{B\pi_1(a, b)} b}

Uniqueness rules for Sigma types:

Γz: x:AB(x)Γη Σ:z= x:AB(x)(π 1(z),π 2(z))\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \eta_\Sigma:z =_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z))}

\section{Pullbacks}

Given two functions fA Bf \in A^B and gA Cg \in A^C, the pullback? of ff and gg is given by the set

bB cCf(b)= Ag(c)\biguplus_{b \in B} \biguplus_{c \in C} f(b) =_A g(c)

\section{Singleton}

Use the negative presentation of a unit type.

Thus, the dependent type theory models a locally cartesian closed category? with pullbacks? and a terminal object?, and the category is thus finitely complete? and cartesian closed?

\section{Set of truth values}

\section{References}

  • Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)

  • Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)

  • Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)

\section{See also}

Revision on November 28, 2022 at 03:48:48 by Anonymous?. See the history of this page for a list of all contributions to it.