## Naïve Type Theory ↑

### Thorsten Altenkirch

#### University of Nottingham

In this course we introduce Type Theory (sometimes called
"dependent type theory") as an informal language for
mathematical constructions in Computer Science and other
disciplines. By Type Theory we mean the constructive fundation
of Mathematics whose development was started by Per
Martin-Loef in the 1970ies based on the Curry-Howard
equivalence of propositions and types. Because of this
proximity to Computer Science, Type Theory has been the
foundation of interactive theorem provers and programming
languages such as NuPRL, Coq, Agda and Idris. While the
calculi on which these systems are based are an important
research topic, in this course we want to emphasise the
"naive" use of Type Theory using just pen and paper. Indeed
this is similar to the naive use of set theory which is
usually applied informally without explicitly relating each
constructions to the axioms of set theory (as in Halmos' book
on "Naive Set Theory").

In this course we focus on the intuitive foundations of
Type Theory and on basic constructions such as: universes,
(dependent) function types, (dependent) products, inductive
types and equality and their use in informal reasoning. If
time permits we will also cover basic constructions from
Homotopy Type Theory, such as the univalence axiom
(isomorphism is equality), and some Higher Inductive Types (a
generalisation of quotient types). A good reference for our
course is chapter 1 of the book on Homotopy Type Theory
(available online).

Course
notes and links