Type Theory and Univalent Mathematics
Introduction
A very informal view of Type Theory
Martin-Löf Type Theory
A minimal Type Theory in Martin-Löf style
2-categorical constructions
Basic 2-categorical constructions
Negation
Negation, decidability, and related propositions
Natural Numbers
definition and properties of the natural numbers
Pointed Types and Loop Spaces
Pointed Types, Loop Spaces, and the Eckmann-Hilton argument
Basic Homotopy
Basic homotopy theory constructions: weak equivalences, homotopy equivalences, homotopy fibers, and type-theoretic constructions inspired by them
Propositions, Sets and Logic
Singletons, Propositions, and Sets. Excluded Middle
Univalence—Ⅰ
Towards the univalence axiom, function extensionality
Function Extensionality
Proof of the equivalence of the various function extensionality axioms
Univalence—Ⅱ
Univalence implies function extensionality
Univalence—Ⅲ
Global univalence and functional extensionality
Propositions, Sets and Logic—Ⅱ
More about Propositions from a univalent point of view
Univalence—Ⅳ
Some corollaries of the univalence and function extensionality axioms
Magmas, Monoids, Groups
First examples of algebraic structures
Leitfaden
Simple Agda experiments
Natural numbers
A simple example where we code the naturals and few other elementary constructions
Propositional Equality
Definition of propositional equality and some simple theorems using it
Associativity of addition
Some additional simple theorems and techniques. We prove that the addition of naturals is associative