Homotopy Type Theory and the "TU Graz HoTT Papers and Books Club"
In 2017 the Russian mathematician and Fields Medalist Vladimir Voevodsky died at age 51. Voevodsky once discovered a severe error in one of his papers that was already published for years which motivated him to learn using the computer proof assistant Coq. A proof assistant is a program which can verify mathematical proofs and also provides assistance in the process of writing the proofs (such as showing which parts are still open). The basis of Coq and of many other proof assistants isn't set theory as one might expect, but type theory (or more specifically: the calculus of inductive constructions, a version of typed lambda calculus), a theory in which the basic objects are not sets but functions with specific "types" of domains and codomains. A typical type theoretic statement might be: If f is a function from A to B ("of type A -> B") and g is a function from B to C, then the composition of g and f is a function from A to C. This may sound trivial but it turns out that a sufficiently rich axiomatic description of the behavior of pure functions (which is typed lambda calculus) can serve as an alternative to set theory as a basis of mathematics that has one decisive advantage: A "proof" of some statement (theorem) is not a meta-object of the theory (as it is in set theory where a "proof" is not a set itself but a sort of "tree" of set theoretic statements) but is itself an object of the theory: in type theory a proposition (theorem) is a type and a proof is a function of that type. The type A -> B of functions from A to B is interpreted as the statement "A implies B" and a function "f:A -> B" that has this type is interpreted as a proof of that statement (it is a function which maps proofs of statement A to proofs of statement B which is exactly what implication means). This is the so-called Curry-Howard isomorphism or PAT interpretation of typed lambda calculus, where PAT stands for both "Propositions As Types" and "Proofs As Terms". It turns out that all of predicate logic and all of mathematics can be encoded in this way just as well as in set theory but with the mentioned advantage of having concrete "proof objects" within the theory, which makes it perfect to be implemented on computers.
When Voevodsky studied type theory in order to understand how Coq works in the background he, being a world-leading expert on homotopy theory, noticed deep connections between the two fields. Homotopy theory is the theory of "shapes" in a topological sense. Two topological spaces are said to be homotopy equivalent if they can be deformed continuously (the continuous maps then being called "homotopies") into each other like a coffee mug and a torus. His observations led to the invention of homotopy type theory (HoTT) and the program of so-called "univalent foundations of mathematics" within the last few years which many think might shape the future of mathematics in the next decades. One of the distant goals is to have set theory replaced by HoTT and to make formalizing and checking mathematical proofs with proof assistants as easy as writing papers in LaTeX. In addition, HoTT reveals deep connections between type theory, functional programming, homotopy theory, logic, and higher order category theory (the typed lambda calculus that is used in HoTT can be interpreted as a so-called "infinity-groupoid" which is a higher order category in which all morphisms are isomorphisms). The purpose of the "TU Graz HoTT Papers and Books Club" is to study this fascinating field. In particular, the seminar has the following goals:
- Reading and understanding at least parts of an introductory book on typed lambda calculus such as "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Geuver.
- Reading and understanding at least parts of an introductory book on homotopy theory such as Algebraic Topology by Allen Hatcher.
- Reading and understanding the HoTT Book on the "univalent foundations of mathematics" which was written by Voevodsky and others.
- Understanding the relations between HoTT and category theory.
- Learning to use the computer proof assistant Coq.
- Have fun!
Literature
Books
- Homotopy Type Theory, Univalent Foundations of Mathematics - The Univalent Foundations Program
- Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers
- Algebraic Topology - Allen Hatcher
- Certified Programming with Dependent Types - Adam Chlipala
- Interactive Theorem Proving and Program Development, Coq'Art, The Calculus of Inductive Constructions - Yves Bertot and Pierre Castéran
- Programming in Haskell - Graham Hutton
- Topoi, The Categorial Analysis of Logic - Robert Goldblatt
- Category Theory in Context - Emily Riehl
Papers
- Introduction to the Calculus of Inductive Constructions - Christine Paulin-Mohring
- Intuitionistic Type Theory - Per Martin-Löf
Activities
- Wednesday, January 24, 2018, 2 p.m.
"Sozialraum" of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Preliminary meeting - Friday, February 2, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
First chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 1-11, up to "1.6 Substitution"
Notes: HoTT Seminar 02.02.2018.pdf, HoTT Seminar 02.02.2018 LaTeX.pdf - Friday, February 16, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
First chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 11-24, up to "1.10 Fixed Point Theorem"
Notes: HoTT Seminar 16.02.2018.pdf - Friday, March 2, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
First chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 24-31, completed first chapter, discussed exercises up to and including 1.14.
Notes: HoTT Seminar 02.03.2018.pdf - Friday, March 23, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Second chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 33-46, up to "2.6 Kinds of problems to be solved in type theory"
Notes: HoTT Seminar 23.03.2018.pdf - Friday, April 6, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Second chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 46-53, up to "2.10 General properties of λ→"
Notes: HoTT Seminar 06.04.2018.pdf - Friday, April 20, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Second chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 53-68, completed second chapter
Notes: HoTT Seminar 20.04.2018.pdf - Friday, May 4, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Third chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 69-78, up to "3.6 Properties of λ2"
Notes: HoTT Seminar 04.05.2018.pdf - Friday, May 18, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Third chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 78-84, completed third chapter
Notes: HoTT Seminar 18.05.2018.pdf - Friday, June 8, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Fourth chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 85-93, up to "4.4 The formation rule in λω"
Notes: HoTT Seminar 08.06.2018.pdf - Friday, June 29, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Fourth chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 93-102, completed fourth chapter
Notes: HoTT Seminar 29.06.2018.pdf - Friday, November 9, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Recapitulation of chapters 1-4 of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 1-102
Notes: HoTT Seminar 09.11.2018.pdf - Friday, December 7, 2018, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Fifth chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 103-109, up to "5.4 Minimal predicate logic in λP"
Notes: HoTT Seminar 07.12.2018.pdf - Friday, January 18, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Fifth chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 109-122, completed fifth chapter
Notes: HoTT Seminar 18.01.2019.pdf - Friday, February 1, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Sixth and seventh chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 123-141, up to "II. Disjunction"
Notes: HoTT Seminar 01.02.2019.pdf - Friday, March 8, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Seventh chapter of "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" on untyped lambda calculus
Pages 142-164, completed seventh chapter
Notes: HoTT Seminar 08.03.2019.pdf - Friday, April 5, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Solving problems from "Type Theory and Formal Proof - Rob Nederpelt and Herman Geuvers" with Coq
Notes: HoTT Seminar 05.04.2019.v - Friday, May 17, 2019, 2 p.m.
Seminar room of the Institute of Statistics (Kopernikusgasse 24, 3rd floor)
First session on homotopy theory - Friday, June 7, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Second session on homotopy theory - Friday, June 28, 2019, 2 p.m.
Seminar room of the Institute of Analysis and Number Theory (Kopernikusgasse 24, 2nd floor)
Third session on homotopy theory