Andrej Bauer: Homotopska teorija tipov v Coq-u

Povzetek: Seminar se navezuje na seminar "Logika iz geometrije", v kateri smo predstavili osnove matematike, ki slonijo na geometrijskem pojmovanju prostorov in konstrukcij. V tokratnem seminarju bomo obrnili pogled v nasprotno smer in dokazovali geometrijske izreke s pomo`čjo logike in aksiomov, ki smo jih predstavili na prvem seminarju. Pri tem bomo uporabljali dokazovalni sistem Coq.

Vabljeni!