# Inductive Type

## Definition

$F(μX.F)→μX.F(X)$$F(X)→X⊢μX.F(X)→X$

[bahareh-afshari-2019]

$F:U→U,(A,B:U)→(A→B)→F(A)→F(B).$$(X:U)→(F(X)→X)→μF→X.$$𝟎,F(𝟎),F(F(𝟎)),…$$(X:U)→(X→F(X))→X→νF.$$𝟏,F(𝟏),F(F(𝟏)),…$

### Induction Principle

$(F(X)→X)→μF→X.$

### Coinduction Principle

$(X→F(X))→X→νF.$

[xavier-leroy-2019]

$𝟏≡νX.X.$$𝟎≡μX.X.$

[bahareh-afshari-2019]

## Inductive Types

Church Data Type (iterative), in λ2

$A≡λX.(F(X)→X)→X$

Scott Data Type (case), in λ2μ

$A≡λX.(F(A)→X)→X$

Church-Scott Data Type (primitive recursive), in λ2μ

$A≡λX.(F(A×X)→X)$

## Coinductive Types

[herman-geuvers-2015]

## μ

### 𝟏+𝟏

𝟐, boolean.

[herman-geuvers-2014]

### 𝟏+A

Option, or maybe.

[andreas-abel-2013]

### 𝟏+X

$ℕ≡μX. 𝟏+X.$

#### Church-Scott

$λA.A→(A→A)→A.$$μX.λA.A→(X→A)→A.$$μX.λA.A→(X→A→A)→A.$

### 𝟏+(A×X)

List.

[thorsten-altenkirch-2004]

#### Church-Scott

$λA.A→(X→A→A)→A$

[herman-geuvers-2014]

### 𝟏+(A×X×X)

Binary tree.

[thorsten-altenkirch-2004]

#### Church-Scott

$λX.(A→X)→(B→X→X→X)→X.$

[herman-geuvers-2014]

### A+(A×X)+(X×X)

Lambda calculus.

[yigal-duppen-2000]

### 𝟏+X+(ℕ→X)

Ordinals.

[thorsten-altenkirch-2004]

### 𝟏+(X×Y)

F tree.

[thorsten-altenkirch-2004]

## ν

### A×X

Stream.

[andreas-abel-2013]

#### Church-Scott

λ2

$∃X.X×(X→A×X)$

λ2μ

$μY.∃X.X×(X→A×(X+Y))$

[herman-geuvers-2014]

### 𝟐×(A→X)

Deterministic automata.

[alexander-kurz-2018]

### A×(B→X)

W-types.

[thorsten-altenkirch-2004]

### μ_.(𝟏+A×X)

Colist.

[andreas-abel-2013]

### ℕ×(μX.𝟏+A×X)

Vector.

[andreas-abel-2013]

## Polynomial Functors

$F(X)≡(a:A)×B(a)→X.$$List(A)≅(n:ℕ)×Fin(n)→A.$

[simon-hudon-2019]

## Quotients of Polynomial Functors

1. $\mathrm{abs}:P\left(A\right)\to F\left(A\right)\text{, (abstraction)}$
2. $\mathrm{repr}:F\left(A\right)\to P\left(A\right)$
3. $\left(x:F\left(A\right)\right)\to \mathrm{abs}\left(\mathrm{repr}\left(x\right)\right)=x\text{.}$

The class of QPFs is closed under:

• composition
• quotients
• initial algebras
• final colagebras

In particular, finset and multiset are QPFs.

[simon-hudon-2019]