Type Theory

Wikipedia nLab

Contents

Wikipedia nLab

Function type.

Formation Rule

A:𝒰 B:𝒰AB:𝒰.

Introduction Rule

λ-abstraction.

a:A b:Bλ(a).b:AB.

Computation Rule

β-conversion or β-reduction.

a:A b:B(λ(a).b)(a)b:B.

Uniqueness Principle

η-conversion or η-expansion.

a:A b:Bbλ(a).b(a):AB.

α-conversion

λ(x).f(x)λ(y).f(y).

Currying

c(a,b)c(a)(b).

Right Associativity

ABCA(BC).

Constant Function

b:B a:Aλ(a).b:AB.

Universe

Introduction Rule

𝒰i:𝒰i+1.

Cumulativity

A:𝒰iA:𝒰i+1.

Dependent Type (type family)

Wikipedia nLab

Finite Set

Fin:𝒰.

Constant Dependent Type

B:𝒰λ(a).B:A𝒰.

Dependent →

Dependent function type, Π-type.

Formation Rule

A:𝒰 a:AB:𝒰(a:A)B:𝒰.

Introduction Rule

a:Ab:Bλ(a:A).b:(a:A)B.

Elimination Rule

b:(a:A)B a:Ab(a):B[a/x].

Computation Rule

Uniqueness Principle

b:(a:A)Bbλ(a).b:(a:A)B.(a:A)BAB(x,y:A)B(x,y)(x:A)(y:A)B(x,y).

Example

fmaxnnn+1:(n:)Fin(n+1).

Polymorphic Function

A:𝒰,x:AidAx.A,B,C:𝒰,c:C|swapbac.

×

Wikipedia nLab

Product type, cartesian product.

Formation Rule

a:A b:BA×B:𝒰.

Introduction Rule

a:A b:B(a,b):A×B.

Recursion Principle

recA×B(C,c,(a,b))c(a)(b),recA×B:(C:𝒰)(ABC)(A×B)C.

Projection

pr1recA×B(A,λ(a).λ(b).a),pr1:A×BA.pr2recA×B(B,λ(a).λ(b).b),pr2:A×BB.

Induction Principle

indA×B(C,c,(a,b))c(a)(b),indA×B:(C:(A×B)𝒰)((a:A)(b:B)C((a,b)))(x:A×B)C(x).

Uniqueness Principle

Propositional uniqueness principle.

uniqA×B((a,b))refl(a,b),uniqA×B:(x:A×B)((pr1(x),pr2(x))=x).

From category-theoretic perspective, we define product A × B to be left adjoint to the 'exponential' B → C.

𝟏

Unit type.

Formation Rule

𝟏:𝒰.

Introduction Rule

*:𝟏.

Recursion Principle

rec𝟏(C,c,*)c,rec𝟏:(C:𝒰)C𝟏C.

Induction Principle

ind𝟏(C,c,*)c,ind𝟏:(C:𝟏𝒰)C(*)(x:𝟏)C(x).

Uniqueness Principle

Propositional uniqueness principle.

uniq𝟏refl*,or uniq𝟏ind𝟏(λ(x).x=*,refl*),uniq𝟏:(x:𝟏)(x=*).

Dependent ×

Dependent pair type, Σ-type.

Formation Rule

A:𝒰 a:AB:𝒰(a:A)×B(a):𝒰.

Introduction Rule

a:AB(a):𝒰 a:A b:B[a/x](a,b):(x:A)×B(x).((a:A)×B)(A×B).pr1((a,b))a,pr1:((a:A)×B(a))A.pr2:(p:(a:A)×B(a))B(pr1(p)).

Recursion Principle

rec(a:A)×B(a)(C,c,(a,b))c(a)(b),rec(a:A)×B(a):(C:𝒰)((a:A)B(a)C)((a:A)×B(a))C.

Induction Principle

Dependent eliminator.

C(p)B(pr1(p)),pr2((a,b))b.ind(a:A)×B(a)(C,c,(a,b))c(a)(b),ind(a:A)×B(a):(C:((a:A)×B(a))𝒰)((a:A)(b:B(a))C((a,b)))(p:(a:A)×B(a))C(p).

Uniqueness Principle

Propositional uniqueness principle.

See homotopy type theory#dependent-×-uniqueness.

Axiom of choice

ac(g)(xpr1(g(x)),xpr2(g(x))),ac:((x:A)(y:B)×R(x,y))((f:AB)×(x:A)R(x,f(x))).

+

Wikipedia nLab

Sum type, coproduct type.

Formation Rule

A:𝒰 B:𝒰A+B:𝒰.

Introduction rules

A:𝒰 B:𝒰 a:Ainl(a):A+B,  A:𝒰 B:𝒰 b:Binr(b):A+B.

Recursion Principle

Case analysis'

recA+B(C,c0,c1,inl(a))c0(a),recA+B(C,c0,c1,inr(b))c1(b),recA+B:(C:𝒰)(AC)(BC)(A+B)C.

Induction Principle

indA+B(C,c0,c1,inl(a))c0(a),indA+B(C,c0,c1,inr(b))c1(b),indA+B:(C:(A+B)𝒰)((a:A)C(inl(a)))((b:B)C(inr(b)))(x:A+B)C(x).

𝟎

Empty type.

Formation Rule

𝟎:𝒰.

Introduction Rule

-.

Recursion Principle

Principle of explosion. Canonical function.

rec𝟎(C,),rec𝟎:(C:𝒰)𝟎C.

Induction Principle

ind𝟎(C,),ind𝟎:(C:𝟎𝒰)(x:𝟎)C(x).

𝟐

Boolean type.

Formation Rule

𝟐:𝒰.

Introduction rules

0𝟐:𝟐,  1𝟐:𝟐.

Recursion Principle

rec𝟐(C,c0,c1,0𝟐)c0,rec𝟐(C,c0,c1,1𝟐)c1,rec𝟐:(C:𝒰)CC𝟐C.

Induction Principle

ind𝟐(C,c0,c1,0𝟐)c0,ind𝟐(C,c0,c1,1𝟐)c1,ind𝟐:(C:𝟐𝒰)C(0𝟐)C(1𝟐)(x:𝟐)C(x).

Natural numbers.

Formation Rule

:𝒰.

Introduction Rules

0:,  n:succ(n):.

Recursion Principle

Primitive recursion.

rec(C,c0,cs,0)c0,rec(C,c0,cs,succ(n))cs(n,rec(C,c0,cs,n)),rec:(C:𝒰)C(CC)C.

Induction Principle

ind(C,c0,cs,0)c0,ind(C,c0,cs,succ(n))cs(n,ind(C,c0,cs,n)),ind:(C:𝒰)C(0)((n:)C(n)C(succ(n)))(n:)C(n).

Uniqueness Principle

Pattern Matching and Recursion

Propositions As Types

EnglishType Theory
True𝟏
False𝟎
A and BA×B
A or BA+B
If A then BAB
A if and only if B(AB)×(BA)
Not AA𝟎
For all a : A, P(a) holds(a:A)P(a)
There exists a : A such that P(a)(a:A)×P(a)
a:A,P,Qa:AP,a:AQ.

=

Identity type.

Formation Rule

A:𝒰 a:A b:Aa=Ab:𝒰.

Introduction Rule

Reflexivity.

A:𝒰 a:Arefla:a=Aa.

Recursion Principle

Indiscernibility of identicals.

rec=A(C,a,a,refla)=C(a),rec=A:(C:A𝒰)(a,b:A)(p:a=Ab)C(a)C(b).

Induction Principle

Path induction.

ind=A(C,c,a,a,refla)c(a),ind=A:(C:(a,b:A)(a=Ab)𝒰)((a:A)C(a,a,refla))(a,b:A)(p:a=Ab)C(a,b,p).

Uniqueness Principle

Inductive Types

nil:Vec0(A),cons:(n:)AVecn(A)Vecsucc(n)(A).C:(n:)Vecn(A)𝒰,cnil:C(0,nil),ccons:(n:N)(a:A)(l:Vecn(A))C(n,l)C(succ(n),cons(a,l)).f:(n:N)(l:Vecn(A))C(n,l),f(0,nil)cnil,f(succ(n),cons(a,l))ccons(n,a,l,f(l)).

Theorem

f,g:(n:)E(n), ez:E(0), es:(n:)E(n)E(succ(n)),f(0)=ez, g(0)=ez,(n:)f(succ(n))=es(n,f(n)), (n:)g(succ(n))=es(n,g(n)),f=g.nil:List(1),cons: 1×List(1)List(1).E:List(1)𝒰,enil:E(nil),econs:(u:1)(l:List(1))E(l)E(cons(u,l)),f:(l:List(1)),f(nil)enil,f(cons(u,l))econs(u,l,f(l)).0''nil,succ''(l)cons(*,l),succ'':List(1)List(1),E:List(1)𝒰,e0:E(0''),es:(l:List(1))E(l)E(succ''(l)),enile0,econs(*,l,x)es(l,x).f(0'')f(nil)enile0,f(succ''(l))f(cons(*,l))econs(*,l,f(l))es(l,f(l)),f:(l:List(1))E(l),List(1)=.

W-Types

Wa:AB(a).wWb:𝟐rec𝟐(𝒰,0,1,b).list(A)Wx:𝟏+Arec𝟏+A(𝒰,0,a1,x).sup:(a:A)(B(a)Wx:AB(x))Wx:AB(x).0wsup(0𝟐,xrec𝟎(w,x)).1wsup(1𝟐,x𝟎w),succwnsup(1𝟐,xn).e:(a:A)(f:B(a)Wx:A B(x))(g:(b:B(a))E(f(b)))E(sup(a,f)).e:(a:𝟐)(f:B(a)w)(g:B(a)w)w.

ℕ-Algebra

Inductive types are homotopy-initial algebras

Definition

ℕAlg(C:𝒰)×C×(CC).

ℕ-homomorphism

Definition

h:CD,h(c0)=d0,h(cs(c))=ds(h(c)) for c:C.NHom((C,c0,cs),(D,d0,ds))(h:CD)×(h(c0)=d0)×(c:C)(h(cs(c))=ds(h(c))).

A natural numbers object in an (∞, 1)-category of N-algebra.

Homotopy-Initial

is-homotopy-initial(I)(c:NAlg)is-truncated−2(NHom(I,C)).

Theorem

is-homotopy-initial((,0,succ)).

N-algebras are the algebras for the endofunctor F(X)X + 1 of the category of types.

Polynomial Functor

P(X)=(a:A)×(B(a)X).

W-Algebra

Also called P-algebra.

WAlg(A,B)(C:𝒰)×(a:A)(B(a)C)C.

W-Homomorphism

Also Called P-homomorphism.

f(sC(a,h))=sD(a,f h).WHomA,B((C,sC),(D,sD))(f:CD)×(a:A)(h:B(a)C)f(sC(a,h))=sD(a,f h).

Homotopy-Inductive Type

The General Syntax of Inductive Definitions

Strict Positivity

Generalisations of Inductive Types

Identity Type and Identity System

Pointed Predicate

(A,a0), R:A𝒰, r0:R(a0).

Pointed

(R,r0),(S,s0), g:(b:A)R(b)S(b), g(a0,r0)=s0.ppmap(R,S)(g:(b:A)R(b)S(b))×(g(a0,r0)=s0).

Identity System

(R,r0)D:(b:A)R(b)𝒰, d:D(a0,r0),f:(b:A)(r:R(b))D(a0,r0),f(a0,r0)=d.

Rational Numbers

(×)/.

Real Numbers

Intensional Type Theory

nLab

References