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

#### Dependent Type (type family)  ### 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.

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

$ℝ$

## Intensional Type Theory 