# nLab definition

There are good reasons why the theorems should all be easy and the definitions hard. (Michael Spivak, preface to “Calculus on Manifolds” )

# Contents

## In type theory

In type theory a definition is the construction of a term of a certain type.

As such definitions are no different from proofs of theorems (due propositions-as-types). For instance the constructive proof that there exists a natural number consists of exhibiting one, and hence the definition of, say $2 \in \mathbb{N}$ is the same as a specific proof that $\exists x \in \mathbb{N}$.

Revised on February 17, 2015 10:12:44 by Urs Schreiber (195.113.30.252)