Date: 27 July 2019

These are draft notes and are not intended to be a complete reference.

Dependent Type theory

Date: 04 September 2019

We sketch an introduction to the concepts of dependent type theory accompanied by idris code. This note does not include propositions as types, which will be in the sequel. This is an annotated version of the live code from the lecture but wih some reordering for a better flow.

Terms and Types

Objects in type theory are called terms. Each term has a type, generally unique. The notation a: A means a is a term of type A. For example Nat is a type and we define a term...

Inductive types and type families

Date: 08 September 2019

Type Theory is a language. We have taken an immersion learning approach to it (as well as to the language of sets) - where we learn a language by listening to it being spoken, relating to known languages and eventually learning the specific idioms. In this note we take a more formal view, looking more explicitly at the rules of the grammar. Hopefully this will complement immersion learning.

Inductive Types: a more formal view

In the flavour of type theory we consider, namely Martin-Löf Type Theory (MLTT), all types are of one of the following forms.

• Universes such...