category: reference J. M. E. Hyland, 27.11.2012, Classical lambda calculus in modern dress, [ arXiv:1211.5762](http://arxiv.org/abs/1211.5762) ## 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$ 1. Lawvere theories) ## 3 The lambda calculus Term formation in Martin-Löf's approach: $$\frac{\Gamma \vdash t\in a\Rightarrow b\;\Gamma\vdash \u\in a}{\Gamma \dashv tu\in b}$$ $$\frac{\Gamma, x\in a\vdash s\in b}{\Gamma \vdash\lambda x.s\in a\Rightarrow b}$$ computation rule: $$(\lambda x.s)u=s[u/x]$$