Naïve Type Theory by Thorsten Altenkirch (University of Nottingham, UK)

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: Naïve Type Theory by Thorsten Altenkirch (University of Nottingham, UK) Abstract: 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 foundation 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 here: ). This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).