Univalent Foundations Project (2010)
Unlike the usual semantics which interpret types as sets,
this ”univalent semantics” interprets types as homotopy types.
The key property of the univalent interpretation is that it satisfies the univalence axiom,
a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences.
Thierry Coquand
Séminaire Bourbaki - 21/06/2014 - 4/4 - Thierry COQUAND : Théorie des types dépendants et axiome d'univalence 02:05
Suggestion possible pour changer les règles de syntaxe de la théorie des ensembles pour exprimer certains phénomènes qui ne sont pas bien exprimés en théorie des ensembles.
C'est le programme de Voevodsky qui consiste à exprimer les mathématiques en utilisant la théorie des types dépendants au lieu de la théorie des ensembles.
Ce programme repose sur les 2 points suivants :
description / vision des mathématiques comme analyse des structures sur les infini-groupoïdes.
La théorie des types dépendants fournit un langage et un système de notations appropriés pour représenter les structures sur les infini-groupoïdes.
12:03 : On introduit un opérateur très naturel en mathématiques, qui est que quand un objet est défini uniquement, alors on peut donner un nom à cet objet.
L'opérateur iota introduit par Church est une formalisation de cette idée.
iota est décrit par l'axiome de description qui dit que s'il y a un unique objet x satisfaisant la propriété phi, alors phi est vraie pour cet objet sélectionné par iota.
Quanta Magazine
Will Computers Redefine the Roots of Math?
Vladimir Voevodsky’s univalent foundations program aims to rebuild mathematics in a way that will allow computers to check all mathematical proofs.
(...) Voevodsky is aware that a new foundation for mathematics is a tough sell, and he admits that “at the
moment there is really more hype and noise than the field is ready for.”