Homotopy Type Theory homotopy type theory > history (changes)

Showing changes from revision #49 to #50: Added | Removed | Changed

\tableofcontents

\section{Idea}

Homotopy type theory is a framework of dependent type theories which additionally consists of

  • identity types

  • dependent product types

  • dependent sum types

  • univalence

  • inductive types, higher inductive types, inductive type families, et cetera.

\section{Presentation}

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

  • Definitional equality is a metatheoretical equivalence relation, in the same way that alpha-equivalence is. Since alpha-equivalence usually isn’t defined as part of the type theory, definitional equality shouldn’t be either. Similarly, the notation \coloneqq used for definitions usually isn’t defined as part of the theory itself either.

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

Homotopy type theory consists of the following judgments:

  • Type judgments, where we judge AA to be a type, AtypeA \; \mathrm{type}

  • Term judgments, where we judge aa to be an element of AA, a:Aa:A

  • Context judgments, where we judge Γ\Gamma to be a context, Γctx\Gamma \; \mathrm{ctx}.

Contexts are lists of term 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 term 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}

Within any dependent type theory, the structural rules include the variable rule?, the weakening rule?, and the substitution rule?.

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

Γ,a:A,ΔctxΓ,a:A,Δa:A\frac{\Gamma, a:A, \Delta \; \mathrm{ctx}}{\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.

\subsection{Sections and dependent types}

A dependent type is a type BtypeB \; \mathrm{type} in the context of the variable judgment x:Ax:A, x:ABtypex:A \vdash B \; \mathrm{type}. A section is a term b:Bb:B in the context of the variable judgment x:Ax:A, x:Ab:Bx:A \vdash b:B.

\subsection{Identity types}

Formation rule for identity 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 identity 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 identity types:

Γ,a:A,b:A,p:a= Ab,Δ(a,b,p)C(a,b,p)typeΓ,a:A,Δ(a,a,refl A(a))t:C(a,a,refl A(a))Γ,a:A,b:A,p:a= Ab,Δ(a,b,p)J(t,a,b,p):C(a,b,p)\frac{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{type} \quad \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash J(t, a, b, p):C(a, b, p)}

Computation rules for identity types:

Γ,a:A,b:A,p:a= Ab,Δ(a,b,p)C(a,b,p)typeΓ,a:A,Δ(a,a,refl A(a))t:C(a,a,refl A(a))Γ,a:A,b:A,p:a= Ab,Δ(a,b,p)β = A(a):J(t,a,a,refl(a))= C(a,a,refl A(a))t\frac{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{type} \quad \Gamma, a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}

\subsection{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))}

\subsection{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)}

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

\subsection{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)}

\subsection{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)}

\subsection{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_*)}

\subsection{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}

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

\subsection{Equivalence types}

Given a type AA, we define the type isContr(A)\mathrm{isContr}(A) representing whether AA is a contractible type as

isContr(A) a:A b:Aa= Ab\mathrm{isContr}(A) \coloneqq \sum_{a:A} \prod_{b:A} a =_A b

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

fiber A,B(f,y) a:Af(a)= Bb\mathrm{fiber}_{A, B}(f, y) \coloneqq \sum_{a:A} f(a) =_B b

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

isEquiv(f) b:BisContr(fiber A,B(f,b))\mathrm{isEquiv}(f) \coloneqq \prod_{b:B} \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, b))

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

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

\subsection{Transport}

Transport is the statement that given a type family PP indexed by AA, elements a:Aa:A and b:Ab:A, and an identification p:a= Abp:a =_A b, there is an equivalence trans P(a,b,p):P(a)P(b)\mathrm{trans}^P(a, b, p):P(a) \simeq P(b) between the types P(a)P(a) and P(b)P(b), and additionally, for all elements a:Aa:A, there is an identification

ind trans P refl A(a):trans P(a,a,refl A(a))= P(a)P(a)id P(a)\mathrm{ind}_{\mathrm{trans}^P}^{\mathrm{refl}_A}(a):\mathrm{trans}^P(a, a, \mathrm{refl}_A(a)) =_{P(a) \simeq P(a)} id_{P(a)}

Transport is given by the following rules:

ΓAtypeΓ,x:APtypeΓa:AΓb:AΓp:a= AbΓtrans P(a,b,p):P[a/x]P[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b}{\Gamma \vdash \mathrm{trans}^P(a, b, p):P[a/x] \simeq P[b/x]}
ΓAtypeΓ,x:APtypeΓa:AΓind trans P refl A(a):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}_A}(a):\mathrm{trans}^P(a, a, \mathrm{refl}_A(a)) =_{P[a/x] \simeq P[a/x]} \mathrm{id}_{P[a/x]}}

Transport is very important in defining higher inductive types.

\subsection{Dependent identity types}

We define the dependent identity type? as follows:

x= P pytrans P(a,b,p)(x)= P(b)yx =_P^p y \coloneqq \mathrm{trans}^P(a, b, p)(x) =_{P(b)} y

\subsection{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{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}

\section{External links}

Last revised on November 28, 2022 at 04:08:03. See the history of this page for a list of all contributions to it.