These are draft notes and are not intended to be a complete reference.
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.
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...
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.
In the flavour of type theory we consider, namely Martin-Löf Type Theory (MLTT), all types are of one of the following forms.