Učitavanje video playera...
01:35:56
Andrej Bauer: Constructions as foundations of mathematics
Abstract: Type theory is a foundation of mathematics which takes as primitive mathematical constructions, rather than logic and collections of objects. That this is possible should not be surprising – after all, constructions of all kinds permeate mathematical activity, and already Euclid's Elements put propositions and constructions on equal footing. However, the standard Martin-Löf type theory lacks certain features that are essential to the development of mathematics, namely extensionality principles, which are akin to Leibniz's identity of indiscernibles. The most interesting and challenging extensionality principle is Voevodsky's Axiom of Univalence, which can be seen as an extensionality principle for the universe of types. Once we set up the new Univalent foundations based on type theory, we discover an amazing connection between mathematical foundations and abstract homotopy theory.
