Martin-LöfTypeTheory

(redirected from Libraries.MLTT)

Agda is essentially an extension of intensional Martin-Löf type theory based on a logical framework. Here we present the standard set formers of Martin-Löf type theory (see for example Martin-Löf 1973, 1979, 1984) and a few definable combinators.

These files can provide a starting point for the logically inclined user who wants to work in a fixed theory with a well-understood metatheory. To work strictly within Martin-Löf type theory means that only explicit definitions (abbreviations) may be used when introducing new notions or proving new theorems. No new data types may be added. Defining functions by pattern matching is not allowed either.

• Martin-Löf type theory. Rules for the standard set formers.
• Some combinators as explicit definitions in Martin-Löf type theory.