# Type Theory

## β

Function type.

### Formation Rule

$A:π° B:π°AβB:π°.$

### Introduction Rule

Ξ»-abstraction.

$a:A b:BΞ»(a).b:AβB.$

### 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):AβB.$

### Ξ±-conversion

$Ξ»(x).f(x)Ξ»(y).f(y).$

### Currying

$c(a,b)β‘c(a)(b).$

### Right Associativity

$AβBβCβ‘Aβ(BβC).$

### Constant Function

$b:B a:AΞ»(a).b:AβB.$

## Universe

### Introduction Rule

$π°i:π°i+1.$

### Cumulativity

$A:π°iA:π°i+1.$

### Finite Set

$Fin:ββπ°.$

### Constant Dependent Type

$B:π°β’Ξ»(a).B:Aβπ°.$

## Dependent β

Dependent function type, Ξ -type.

### Formation Rule

$A:π° a:Aβ’B:π°(a:A)βB:π°.$

### Introduction Rule

$a:Aβ’b:BΞ»(a:A).b:(a:A)βB.$

### Elimination Rule

$b:(a:A)βB a:Ab(a):B[a/x].$



### Uniqueness Principle

$b:(a:A)βBbβ‘Ξ»(a).b:(a:A)βB.$$(a:A)βBβ‘AβB(x,y:A)βB(x,y)β‘(x:A)β(y:A)βB(x,y).$

#### Example

$fmaxβ‘nβ¦nn+1:(n:β)βFin(n+1).$

### Polymorphic Function

$A:π°,x:AidAβ‘x.$$A,B,C:π°,c:C|swapβ‘bβaβc.$

## Γ

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:π°)β(AβBβC)β(AΓB)βC.$

### Projection

$pr1β‘recAΓB(A,Ξ»(a).Ξ»(b).a),pr1:AΓBβA.pr2β‘recAΓB(B,Ξ»(a).Ξ»(b).b),pr2:AΓBβB.$

### 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:Aβ’B:π°(a:A)ΓB(a):π°.$

### Introduction Rule

$a:Aβ’B(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 this.

### Axiom of choice

$ac(g)β‘(xβ¦pr1(g(x)),xβ¦pr2(g(x))),ac:((x:A)β(y:B)ΓR(x,y))β((f:AβB)Γ(x:A)βR(x,f(x))).$

## +

Sum type, coproduct type.

### Formation Rule

$A:π° 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:π°)β(AβC)β(BβC)β(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

$π:π°.$

### Recursion Principle

$recπ(C,c0,c1,0π)β‘c0,recπ(C,c0,c1,1π)β‘c1,recπ:(C:π°)βCβCβπβ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

$β:π°.$

### 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β(ββCβC)βββ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).$

## Propositions As Types

EnglishType Theory
True$π$
False$π$
A and B$AΓB$
A or B$A+B$
If A then B$AβB$
A if and only if B$(AβB)Γ(BβA)$
Not A$Aβπ$
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,Qβa:AβP,a:AβQ.$

## =

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).$



## Inductive Types

$nil:Vec0(A),cons:(n:β)βAβ$$Vecn(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)),enilβ‘e0,econs(*,l,x)β‘es(l,x).f(0'')β‘f(nil)β‘enilβ‘e0,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).$$βwβ‘Wb:πrecπ(π°,0,1,b).$$list(A)β‘Wx:π+Arecπ+A(π°,0,aβ¦1,x).$$sup:(a:A)β(B(a)βWx:AB(x))βWx:AB(x).$$0wβ‘sup(0π,xβ¦recπ(βw,x)).$$1wβ‘sup(1π,xβ¦πw),succwβ‘nβ¦sup(1π,xβ¦n).$$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.$

### Inductive types are homotopy-initial algebras

#### Definition

$βAlgβ‘(C:π°)ΓCΓ(CβC).$

### β-homomorphism

#### Definition

$h:CβD,h(c0)=d0,h(cs(c))=ds(h(c)) for c:C.$$NHom((C,c0,cs),(D,d0,ds))β‘(h:CβD)Γ(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:CβD)Γ(a:A)β(h:B(a)βC)βf(sC(a,h))=sD(a,f h).$

## Homotopy-Inductive Type

### 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

$β$