Steve Awodey: Homotopy Type Theory

Datum objave: 15. 6. 2011

Seminar za temelje matematike in teoretično računalništvo

Petek, 17. 6., od 10h do 12h, učilnica 3.04, Jadranska 21

[Pozor: ta teden bo seminar za osnove v petek 17.6. ob 10h v učilnici 3.04 na Jadranski 21, ker bo na obisku prof. dr. Steve Awodey iz Carnegie Mellon University.]

Homotopy Type Theory

Steve Awodey
Carnegie Mellon University
Pittsburgh, ZDA

Abstract: Homotopy type theory refers to a new interpretation of Martin-Löf's system of intensional, constructive type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. In parallel, Vladimir Voevodsky (IAS) has recently proposed a comprehensive, computational foundation for mathematics based on this homotopical interpretation of type theory. The Univalent Foundations Program posits a new "univalence axiom" relating propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq. This talk will survey some of these recent developments.

Prof. Awodey je vodilni raziskovalec na področju teorije kategorij in logike. Pred leti je s svojimi študenti odkril povezavo med teorijo tipov in homotopijo, ki jo postala zelo aktivno področje raziskav, v katerem sodelujejo nekateri najbolj vidni matematiki.

Vabljeni!