Victor Delage
(ILLC)
The Dark Side of the Foundations
May 12th at 18:00, in F1.15
It is a period of civil war. Type theorists, striking from a hidden HoTT base, have won their first victory against the evil set theorists. During the battle, HoTT-spies managed to steal the secret of set theory’s ultimate axiom: the axiom of choice, an armored formula with enough force to reassemble a single death star into two replicas of equal power. Pursued by set theorists, Prince Voevodsky races home aboard his homotopy type theory, custodian of the stolen secret that can bring user-friendliness to proof assistants and restore computability to the implicit foundations of mathematics.