# Church encodings and naturality

## Fredrik Nordvall Forsberg

(University of Strathclyde)

Church encodings can be used to construct weakly initial algebras in

impredicative type systems such as System F or the Calculus of

Constructions. In the latter, we can also ask whether the induction

principle for the data type is derivable, but a result by Herman

Geuvers says that this is never the case, no matter which encoding is

used. However, if we add identity types to the (extensional) Calculus

of Constructions, this changes: by cutting down the Church encoding

to only the "natural transformations", we can construct strongly

initial algebras of arbitrary (even non-strictly positive) functors.

I'll give an introduction to impredicative encodings, and then

consider a baby version of the above result, and how it can be

extended to intensional type theories.

**Friday 21st August 2015, 15:30**

Board Room

Department of Computer Science