Spahn classical lambda calculus in modern dress (Rev #2, changes)

2. Algebraic theories

An algebraic theory is a functor $Fin Set\to Set$.

2.1 Algebraic theories as cartesian operads

2.2 Algebras for theories

2.3 The pre sheaf topos

2.4 Monads and Lawvere theories

(some comments on two classical approaches which are not used in the paper:

1. monads on $Set$ whose functor part is given by the coend formula $T(A)=\int^n \mathcal{T}(n)\times A^n$

2. Lawvere theories)

3 The lambda calculus

Term formation in Martin-Löf’s approach:

computation rule: