definition

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

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

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}$.

Last revised on February 17, 2015 at 10:12:44. See the history of this page for a list of all contributions to it.