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
23kmc.copernicuscenter.edu.pl
www.adamwalanus.pl/2019/konfm...

[@markettinger2147]

This lecture is filled with deep insights that, for me, only reveal themselves upon multiple viewings. Thank you so much!

[@roberttumidalski4713]

👍

[@1330m]

so nice . very informative mathematical kabbalah Category theory proves alpha=omega uroboros. 1st century Israel = 21st century Korea . You have to know that . Amazing historical events are taking place there . Longitude 127 Seoul Okinawa Soul Axis -- Bahai Faith Rael Jesus Huh kyung young Magnificent aletheia .

[@roberttumidalski4713]

Nurnberg.Europ.

[@brendawilliams8062]

Maybe the lord put things in a circl so that man would not know the beginning from the end. True or false. To the thinker.