Intensionality, Invariance, and Univalence, Steve Awodey

What does a mathematical proposition mean? Under one standard account, all true mathematical statements mean the same thing, namely True. A more meaningful account is provided by the Propositions-As-Types conception of type theory, according to which the meaning of a proposition is its collection of proofs. The new system of Homotopy Type Theory provides a further refinement: The meaning of a proposition is the homotopy type of its proofs. A homotopy type may be seen as an infinite-dimensional structure, consisting of objects, isomorphisms, isomorphisms of isomorphisms, etc. Such structures represent systems of objects together with all of their higher symmetries. The language of Martin-Löf type theory is an invariant of all such higher symmetries, a fact which is enshrined in the celebrated Principle of Univalence. Krakow Methodological Conference: 2019 is financed from the funds of the Minister of Science and Higher Education allocated to the dissemination of science [761/P-DUN/2019]. Krakow Methodological Conference: 2019 - zadanie finansowane w ramach umowy 761/P-DUN/2019 ze środków Ministra Nauki i Szkolnictwa Wyższego przeznaczonych na działalność upowszechniającą naukę. #CategoryTheory #KrakowMethodologicalConference https://23kmc.copernicuscenter.edu.pl https://www.adamwalanus.pl/2019/konfmet/index.html