Completed
Dependent types in pictures
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Univalent Foundations and the Equivalence Principle - Benedikt Ahrens
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 What is a foundation of mathematics?
- 3 Outline
- 4 Indiscernability of identicals
- 5 Violating the equivalence principle
- 6 Voevodsky's homotopy lambda calculus
- 7 Overview of type theory
- 8 Dependent types and functions
- 9 Syntax of type theory
- 10 Type dependency
- 11 Dependent types in pictures
- 12 Inference rules and derivations
- 13 The singleton type
- 14 The type of dependent pairs
- 15 The type of dependent functions IL
- 16 A dependent function in pictures
- 17 The identity type
- 18 Some terms that can be defined
- 19 Contractible types, propositions and sets
- 20 Equivalences
- 21 The path type of pairs
- 22 Axioms to characterize some path types
- 23 Transport along isomorphism
- 24 Monoids in type theory
- 25 The type of monoids
- 26 Monoid isomorphisms
- 27 Equivalence principle for set-level structures
- 28 EP for categories
- 29 Conclusions
