Some type theories can serve as an alternative foundation of mathematics, as opposed to standard set theory. One such well-known type theory is Martin-Löf’s intuitionistic theory of types, which is an extension of Alonzo Church’s simply-typed λ-calculus. Before you begin working with Idris, you will become familiar with the theories upon which Idris is built as a language.
![](/api/v2/epubs/9781484292594/files/images/602227_1_En_3_Chapter/602227_1_En_3_Figa_HTML.gif)