Intuitionistic Type Theory Quotes

“We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type [… and] is always given together with its type. … A type is defined by describing what we have to do in order to construct an object of that type. … Put differently, a type is well-defined if we understand … what it means to be an object of that type. Thus, for instance N→N [functions from N to N] is a type, not because we know particular number theoretic functions like the primitive recursive ones, but because we think we understand the notion of number theoretic function in general.”
― Per Martin-Löf, Intuitionistic Type Theory