Homotopy Type Theory dependent type theory > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

\tableofcontents

\section{Idea}

This Dependent article is about dependent type theories, theory which is the foundations for the rest of mathematics mathematics.

time to copy half the homotopy type theory article over here.

\section{Presentation}

The model of dependent type theory we shall be presenting here is the objective type theory version of dependent type theory. There are multiple reasons for this:

  • Since objective type theory lacks definitional equality,

    • The ruleset is simpler in the objective type theory model of homotopy type theory than other models such as Martin-Löf type theory, cubical type theory, or higher observational type theory

    • The results in objective type theory are more general than in models which use definitional equality

    • It is similar to other non-type theory foundations such as the various flavors of set theory, since it also only has one notion of equality, which is propositional equality in both objective type theory and set theory, and uses propositional equality to define terms and types.

  • From a more practical standpoint, objective type theory not only has decidable type checking, it has polynomial (quadratic) time type checking, which makes it efficient from a computational standpoint.

\subsection{Judgments and contexts}

Objective type theory consists of three judgments: type judgments AtypeA \; \mathrm{type}, where we judge AA to be a type, typing judgments, where we judge aa to be an element of AA, a:Aa:A, and context judgments, where we judge Γ\Gamma to be a context, Γctx\Gamma \; \mathrm{ctx}. Contexts are lists of typing judgments a:Aa:A, b:Bb:B, c:Cc:C, et cetera, and are formalized by the rules for the empty context and extending the context by a typing judgment

()ctxΓctxΓAtype(Γ,a:A)ctx\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a:A) \; \mathrm{ctx}}

\subsection{Structural rules}

There are three structural rules in objective type theory, the variable rule?, the weakening rule?, and the substitution rule?.

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

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

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

The weakening rule:

Γ,Δ𝒥ΓAtypeΓ,a:A,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, \Delta \vdash \mathcal{J}}

The substitution rule:

Γa:AΓ,b:A,Δ𝒥Γ,Δ[a/b]𝒥[a/b]\frac{\Gamma \vdash a:A \quad \Gamma, b: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.

There are other rules which could be derived from the three rules above. These include the exchange rule and the variable conversion rule.

The exchange rule:

\subsection{Dependent types and sections}

A dependent type is a type BB in the context of the variable judgment x:Ax:A, x:ABtypex:A \vdash B \; \mathrm{type}, they are usually written as B(x)B(x) to indicate its dependence upon xx.

A section or dependent term is a term b:Bb:B in the context of the variable judgment x:Ax:A, x:Ab:Bx:A \vdash b:B. Sections are likewise usually written as b(x)b(x) to indicate its dependence upon xx.

\subsection{Equality}

Equality of elements of a type in objective type theory is represented by a type known as the equality type or the type of equalities. The elements of the equality type are called equalities.

Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:

Formation rule for equality types:

ΓAtypeΓ,a:A,b:Aa= Abtype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a =_A b \; \mathrm{type}}

Introduction rule for equality types:

ΓAtypeΓ,a:Arefl A(a):a= Aa\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}

Elimination rule for equality types:

Γ, a x:A, b y:A,p: a x= A b yC(a,b,p)typeΓ,a:At:C ( [a,a,refl A(a) ) /x,y,p]Γ, a x:A, b y:A,p: a x= A b yJ(t, a x, b y,p):C(a,b,p) \frac{\Gamma, a:A, x:A, b:A, y:A, p:a p:x =_A b y \vdash C(a, C b, p) \mathrm{type} \quad \Gamma, a:A \vdash t:C(a, t:C[a, a, \mathrm{refl}_A(a))}{\Gamma, \mathrm{refl}_A(a)/x, a:A, y, b:A, p]}{\Gamma, p:a x:A, y:A, p:x =_A b y \vdash J(t, a, x, b, y, p):C(a, p):C} b, p)}

Computation rules for equality types:

Γ, a x:A, b y:A,p: a x= A b yC(a,b,p)typeΓ,a:At:C ( [a,a,refl A(a) ) /x,y,p]Γ,a:A,b:A,p:a= Abβ = A(a):J(t,a,a,refl(a))= C ( [a,a,refl A(a) ) /x,y,p]t \frac{\Gamma, a:A, x:A, b:A, y:A, p:a p:x =_A b y \vdash C(a, C b, p) \; \mathrm{type} \quad \Gamma, a:A \vdash t:C(a, t:C[a, a, \mathrm{refl}_A(a))}{\Gamma, \mathrm{refl}_A(a)/x, a:A, y, b:A, p]}{\Gamma, p:a a:A =_A b \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, =_{C[a, a, \mathrm{refl}_A(a))} \mathrm{refl}_A(a)/x, y, p]} t}

Optional uniqueness rules for equality types:

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

The uniqueness rule for equality types is usually not included in objective type theory. However, if it were included in objective type theory it turns the type theory into a set-level type theory?.

Structural rules for definitions

Now that we have finally defined equality types, we can define the structural rules for definitions. The structural rules for term definitions say that given a term a:Aa:A and a term definition ba:Ab \coloneqq a:A, one could derive that bb is a term of AA, and that there is an equality between bb and aa:

Γa:AΓba:AΓb:AΓa:AΓba:AΓδ A(a,b):b= Aa\frac{\Gamma \vdash a:A \quad \Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b \coloneqq a:A}{\Gamma \vdash \delta_A(a, b):b =_A a}

The structural rules for type definitions are the natural deduction rules for copying? types, with formation and introduction rules:

ΓAtypeΓBAtypeΓBtypeΓAtypeΓBAtypeΓa:AΓcopy(a):B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{copy}(a):B}

elimination rules:

ΓAtypeΓBAtypeΓ,z:BCtypeΓ,x:Ac:C[copy(x)/z]Γe:BΓind B C(c,e):C[e/z]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type} \quad \Gamma, z:B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{copy}(x)/z] \quad \Gamma \vdash e:B}{\Gamma \vdash \mathrm{ind}_{B}^C(c, e):C[e/z]}

computation rules:

ΓAtypeΓBAtypeΓ,z:BCtypeΓ,x:Ac:C[copy(x)/z]Γa:AΓβ B:ind B C(c,copy(a))= C[copy(a)/z]c[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type} \quad \Gamma, z:B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{copy}(x)/z] \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_B:\mathrm{ind}_{B}^C(c, \mathrm{copy}(a)) =_{C[\mathrm{copy}(a)/z]} c[a/x]}

and uniqueness rules:

ΓAtypeΓBAtypeΓ,z:BCtypeΓ,x:Ac:C[copy(x)/z]Γe:BΓ,y:Bu:CΓ,a:Ai copy(u):u[copy(a)/y]= C[copy(a)/y]c[a/x]Γη B:u[e/z]= C[e/z]ind B C(c,e)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \coloneqq A \; \mathrm{type} \quad \Gamma, z:B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{copy}(x)/z] \quad \Gamma \vdash e:B \quad \Gamma, y:B \vdash u:C \quad \Gamma, a:A \vdash i_\mathrm{copy}(u):u[\mathrm{copy}(a)/y] =_{C[\mathrm{copy}(a)/y]} c[a/x]}{\Gamma \vdash \eta_{B}:u[e/z] =_{C[e/z]} \mathrm{ind}_{B}^C(c, e)}

Function types

Formation rules for function types:

ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}

Introduction rules for function types:

Γ,x:Ab(x):BΓ(xb(x)):AB\frac{\Gamma, x:A \vdash b(x):B}{\Gamma \vdash (x \mapsto b(x)):A \to B}

Elimination rules for function types:

Γf:ABΓa:AΓf(a):B\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B}

Computation rules for function types:

Γ,x:Ab(x):BΓa:AΓβ :(xb(x))(a)= Bb\frac{\Gamma, x:A \vdash b(x):B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\to}:(x \mapsto b(x))(a) =_{B} b}

Uniqueness rules for function types:

Γf:ABΓη :f= AB(xf(x))\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash \eta_{\to}:f =_{A \to B} (x \to f(x))}

Pi types

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

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

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

Sum types

Formation rules for sum types:

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

Introduction rules for sum types:

Γa:AΓinl(a):A+BΓb:BΓinr(b):A+B\frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{inl}(a):A + B} \qquad \frac{\Gamma \vdash b:B}{\Gamma \vdash \mathrm{inr}(b):A + B}

Elimination rules for sum types:

Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γe:A+BΓind A+B C(c(x),d(y),e):C(e)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B}{\Gamma \vdash \mathrm{ind}_{A + B}^C(c(x), d(y), e):C(e)}

Computation rules for sum types:

Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γa:AΓβ 1:ind A+B C(c(x),d(y),inl(a))= C(inl(a))c(a)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_1:\mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inl}(a)) =_{C(\mathrm{inl}(a))} c(a)}
Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γb:BΓβ 2:ind A+B C(c(x),d(y),inr(b))= C(inr(b))d(b)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_2:\mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inr}(b)) =_{C(\mathrm{inr}(b))} d(b)}

Uniqueness rules for sum types:

Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γe:A+BΓ,x:A+Bu:CΓ,a:Ai inl(u):u(inl(a))= C(inl(a))c(a)Γ,b:Bi inr(u):u(inr(b))= C(inr(b))d(b)Γη A+B:u(e)= C(e)ind A+B C(c(inl(e)),d(inl(e)),e)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B \quad \Gamma, x:A + B \vdash u:C \quad \Gamma, a:A \vdash i_\mathrm{inl}(u):u(\mathrm{inl}(a)) =_{C(\mathrm{inl}(a))} c(a) \quad \Gamma, b:B \vdash i_\mathrm{inr}(u):u(\mathrm{inr}(b)) =_{C(\mathrm{inr}(b))} d(b)}{\Gamma \vdash \eta_{A + B}:u(e) =_{C(e)} \mathrm{ind}_{A + B}^C(c(\mathrm{inl}(e)), d(\mathrm{inl}(e)), e)}

Empty type

Formation rules for the empty type:

ΓctxΓ𝟘type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0} \; \mathrm{type}}

Elimination rules for the empty type:

Γ,x:𝟘CtypeΓp:𝟘Γind 𝟘 C(p):C(p)\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0}}{\Gamma \vdash \mathrm{ind}_\mathbb{0}^C(p):C(p)}

Uniqueness rules for the empty type:

Γ,x:𝟘CtypeΓp:𝟘Γ,x:𝟘u:CΓη 𝟘(p,u):u[p/x]= C[p/x]ind 𝟘 C(p)\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0} \quad \Gamma, x:\mathbb{0} \vdash u:C}{\Gamma \vdash \eta_\mathbb{0}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{0}^{C}(p)}

Unit type

Formation rules for the unit type:

ΓctxΓ𝟙type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1} \; \mathrm{type}}

Introduction rules for the unit type:

ΓctxΓ*:𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash *:\mathbb{1}}

Elimination rules for the unit type:

Γ,x:𝟙CtypeΓc *:C[*/x]Γp:𝟙Γind 𝟙 C(p,c *):C[p/x]\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1}}{\Gamma \vdash \mathrm{ind}_\mathbb{1}^C(p, c_*):C[p/x]}

Computation rules for the unit type:

Γ,x:𝟙CtypeΓc *:C[*/x]Γβ 𝟙:ind 𝟙 C(*,c *)= C[*/x]c *\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x]}{\Gamma \vdash \beta_\mathbb{1}: \mathrm{ind}_\mathbb{1}^C(*, c_*) =_{C[*/x]} c_*}

Uniqueness rules for the unit type:

Γ,x:𝟙CtypeΓc *:C[*/x]Γp:𝟙Γ,x:𝟙u:CΓi *(u):u[*/x]= C[*/x]c *Γη 𝟙(p,u):u[p/x]= C[p/x]ind 𝟙 C(p,c *)\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1} \quad \Gamma, x:\mathbb{1} \vdash u:C \quad \Gamma \vdash i_*(u):u[*/x] =_{C[*/x]} c_* }{\Gamma \vdash \eta_\mathbb{1}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{1}^{C}(p, c_*)}

Booleans

Formation rules for the booleans:

ΓctxΓ𝟚type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2} \; \mathrm{type}}

Introduction rules for the booleans:

ΓctxΓ0:𝟚ΓctxΓ1:𝟚\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{2}}

Elimination rules for the booleans:

Γ,x:𝟚CtypeΓc 0:C[0/x]Γc 1:C[1/x]Γp:𝟚Γind 𝟚 C(p,c 0,c 1):C[p/x]\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x] \quad \Gamma \vdash p:\mathbb{2}}{\Gamma \vdash \mathrm{ind}_\mathbb{2}^{C}(p, c_0, c_1):C[p/x]}

Computation rules for the booleans:

Γ,x:𝟚CtypeΓc 0:C[0/x]Γc 1:C[1/x]Γβ 𝟚 0:ind 𝟚 C(0,c 0,c 1)= C[0/x]c 0\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x]}{\Gamma \vdash \beta_\mathbb{2}^{0}: \mathrm{ind}_\mathbb{2}^{C}(0, c_0, c_1) =_{C[0/x]} c_0}
Γ,x:𝟚CtypeΓc 0:C[0/x]Γc 1:C[1/x]Γβ 𝟚 1:ind 𝟚 C(1,c 0,c 1)= C[1/x]c 1\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x]}{\Gamma \vdash \beta_\mathbb{2}^{1}: \mathrm{ind}_\mathbb{2}^{C}(1, c_0, c_1) =_{C[1/x]} c_1}

Uniqueness rules for the booleans:

Γ,x:𝟚CtypeΓc 0:C[0/x]Γc 1:C[1/x]Γp:𝟚Γ,x:𝟚u:CΓi 0(u):u[0/x]= C[0/x]c 0Γi 1(u):u[1/x]= C[1/x]c 1Γη 𝟚(p,u):u[p/x]= C[p/x]ind 𝟚 C(p,c 0,c 1)\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x] \quad \Gamma \vdash p:\mathbb{2} \quad \Gamma, x:\mathbb{2} \vdash u:C \quad \Gamma \vdash i_0(u):u[0/x] =_{C[0/x]} c_0 \quad \Gamma \vdash i_1(u):u[1/x] =_{C[1/x]} c_1}{\Gamma \vdash \eta_\mathbb{2}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{2}^{C}(p, c_0, c_1)}

\subsection{Natural numbers}

The natural numbers are the first type introduced in mathematics, so it would be appropriate to introduce them here as well.

Formation rules for the natural numbers:

ΓctxΓtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}

Introduction rules for the natural numbers:

ΓctxΓ0:Γn:Γs(n):\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(n):\mathbb{N}}

Elimination rules for the natural numbers:

Γ,x:CtypeΓc 0:C[0/x]Γ,x:,c:Cc s:C[s(x)/x]Γn:Γind C(n,c 0,c s):C[n/x]\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s):C[n/x]}

Computation rules for the natural numbers:

Γ,x:C(x)typeΓc 0:C(0)Γ,x:,c:Cc s:C[s(x)/x]Γβ 0:ind C(0,c 0,c s)= C[0/x]c 0\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \beta_\mathbb{N}^{0}: \mathrm{ind}_\mathbb{N}^C(0, c_0, c_s) =_{C[0/x]} c_0}
Γ,x:C(x)typeΓc 0:C(0)Γ,x:,c:Cc s:C[s(x)/x]Γβ s(n):ind C(s(n),c 0,c s)= C[s(n)/x]c s(n,ind C(n,c 0,c s))\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \beta_\mathbb{N}^{s(n)}: \mathrm{ind}_\mathbb{N}^C(s(n), c_0, c_s) =_{C[s(n)/x]} c_s(n, \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s))}

Uniqueness rules for the natural numbers:

Γ,x:CtypeΓc 0:C[0/x]Γ,x:,c:Cc s:C[s(x)/x]Γn:Γ,x:u:CΓi 0(u):u[0/x]= C[0/x]c 0Γ,x:i s(u):u[s(x)/x]= C[s(x)/x]c s[u/c]Γη (n,u):u[n/x]= C[n/x]ind C(p,c 0,c s)\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N} \quad \Gamma, x:\mathbb{N} \vdash u:C \quad \Gamma \vdash i_0(u):u[0/x] =_{C[0/x]} c_0 \quad \Gamma, x:\mathbb{N} \vdash i_s(u):u[s(x)/x] =_{C[s(x)/x]} c_s[u/c]}{\Gamma \vdash \eta_\mathbb{N}(n, u):u[n/x] =_{C[n/x]} \mathrm{ind}_\mathbb{N}^{C}(p, c_0, c_s)}

\subsubsection{Addition}

Equivalence types

Addition Given on a the type natural numbers is defined by the following rules:AA, we define the type isContr(A)\mathrm{isContr}(A) representing whether AA is a contractible type as

Introduction rules for addition on the natural numbers:

isContr(A) a:A b:Aa= Ab\mathrm{isContr}(A) \coloneqq \sum_{a:A} \prod_{b:A} a =_A b
Γm:Γn:Γm+n:\frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m + n:\mathbb{N}}

Given types AA and BB, function f:ABf:A \to B, and element b:Bb:B, we define the fiber of ff at bb fiber A,B(f,y)\mathrm{fiber}_{A, B}(f, y) as

Computation rules for addition on the natural numbers:

fiber A,B(f,y) a:Af(a)= Bb\mathrm{fiber}_{A, B}(f, y) \coloneqq \sum_{a:A} f(a) =_B b
ΓctxΓbasecase +:0+0= 0Γm:Γn:Γindcaseleft +(m,n):s(m)+n= s(m+n)Γm:Γn:Γindcaseright +(m,n):m+s(n)= s(m+n)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{basecase}_{+}:0 + 0 =_{\mathbb{N}} 0} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcaseleft}_{+}(m, n):s(m) + n =_{\mathbb{N}} s(m + n)} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcaseright}_{+}(m, n):m + s(n) =_{\mathbb{N}} s(m + n)}

Given types AA and BB and function f:ABf:A \to B, we define the type isEquiv(f)\mathrm{isEquiv}(f) representing whether ff is a equivalence of types? as

\begin{theorem} Addition is associative:

isEquiv(f) b:BisContr(fiber A,B(f,b))\mathrm{isEquiv}(f) \coloneqq \prod_{b:B} \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, b))
Γm:Γn:Γp:Γassoc +(m,n,p):(m+n)+p= m+(n+p)\frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash p:\mathbb{N}}{\Gamma \vdash \mathrm{assoc}_{+}(m, n, p):(m + n) + p =_\mathbb{N} m + (n + p)}

Given types AA and BB, we define the type of equivalences ABA \simeq B as

\end{theorem}

AB f:ABisEquiv(f)A \simeq B \coloneqq \sum_{f:A \to B} \mathrm{isEquiv}(f)

\begin{proof} The equivalence \end{proof} types between two typesAA and BB behaves as the equality between AA and BB, in the same way that the identity type between two terms a:Aa:A and b:Ab:A behaves as the equality between aa and bb. This is similar to structural set theory? whose type of sets have no primitive equality relation, where bijection? behaves as the equality between sets AA and BB.

\subsubsection{Multiplication}

Transport

Multiplication Transport on the natural numbers is defined by the following statement rules: that given a type familyPP indexed by AA and elements a:Aa:A and b:Ab:A, there is a function trans P(a,b):(a= Ab)(P(a)P(b))\mathrm{trans}^P(a, b):(a =_A b) \to (P(a) \simeq P(b)) from the identity type of aa and bb to the type of equivalences between the types P(a)P(a) and P(b)P(b). This is inductively defined on reflexivity on a:Aa:A, which transport takes to the identity function on P(a)P(a), trans P(a,a,refl A(a))= P(a)P(a)id P(a)\mathrm{trans}^P(a, a, \mathrm{refl}_A(a)) =_{P(a) \simeq P(a)} id_{P(a)}.

Introduction Transport rules is for given multiplication by on the natural following numbers: rules:

Γ m AtypeΓ,x: APtypeΓ n a: AΓb:AΓmtrans P × ( n a,b):(a= Ab)(P[a/x]P[b/x]) \frac{\Gamma \vdash m:\mathbb{N} A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{type} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma a:A \quad \Gamma \vdash m b:A}{\Gamma \times \vdash n:\mathbb{N}} \mathrm{trans}^P(a, b):(a =_A b) \to (P[a/x] \simeq P[b/x])}
ΓAtypeΓ,x:APtypeΓa:AΓind trans P refl:trans P(a,a)(refl A(a))= P[a/x]P[a/x]id P[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{ind}_{\mathrm{trans}^P}^{\mathrm{refl}}:\mathrm{trans}^P(a, a)(\mathrm{refl}_A(a)) =_{P[a/x] \simeq P[a/x]} \mathrm{id}_{P[a/x]}}

Computation rules for multiplication on the natural numbers:

Transport is very important in defining univalent Tarski universes? as well as dependent identity types?, which in turn are important in defining higher inductive types, in objective type theory.

Γm:Γbasecase ×(m):m×0= 0Γm:Γn:Γindcase ×(m,n):m×s(n)= m×n+m\frac{\Gamma \vdash m:\mathbb{N}}{\Gamma \vdash \mathrm{basecase}_{\times}(m):m \times 0 =_{\mathbb{N}} 0} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcase}_{\times}(m, n):m \times s(n) =_{\mathbb{N}} m \times n + m}

Dependent identity types

We define the dependent identity type? as follows:

Γa:AΓb:AΓp:a= AbΓx:P(a)Γy:P(b)Γx= P pytrans P(p)(x)= P(b)ytype\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash x:P(a) \quad \Gamma \vdash y:P(b)}{\Gamma \vdash x =_P^p y \coloneqq \mathrm{trans}^P(p)(x) =_{P(b)} y \; \mathrm{type}}

Dependent actions on identifications

Additionally, for a term f:Pf:P in the context of x:Ax:A, there is a dependent identification? called the dependent action on identifications? apd(f)(p):f(x)= P pf(y)\mathrm{apd}(f)(p):f(x) =_P^p f(y) for all x:Ax:A, y:Ay:A, and p:x= Ayp:x =_A y, inductively defined by reflexivity for all x:Ax:A.

apd(f)(refl A(x)):f(x)= P refl A(x)f(x)\mathrm{apd}(f)(\mathrm{refl}_A(x)):f(x) =_P^{\mathrm{refl}_A(x)} f(x)

The rules for apd\mathrm{apd} are as follows

ΓAtypeΓ,x:Af:PΓ,x:A,y:A,p:x= Ayapd(f)(p):f(x)= P pf(y)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash f:P}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{apd}(f)(p):f(x) =_P^p f(y)}
ΓAtypeΓ,x:Af:PΓ,x:Aapd(f)(refl A(x)):f(x)= P refl A(x)f(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash f:P}{\Gamma, x:A \vdash \mathrm{apd}(f)(\mathrm{refl}_A(x)):f(x) =_P^{\mathrm{refl}_A(x)} f(x)}

\section{See also}

\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{External links}

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