Andrej Bauer: Impredicative encodings

Datum objave: 12. 5. 2014
Seminar za temelje matematike in teoretično računalništvo
Torek, 13. 5. 2014, od 12h do 14h, Plemljev seminar, Jadranska 19

Abstract: Impredicative encodings are a logician's trick that allows them to encode logical connectives and quantifiers using just ⇒ and ∀. In computer science it can be used to represent datatypes in terms of polymorphic functions. In homotopy type theory we can use impredicative encodings to encode certain higher-inductive types, such as the circle. We thus obtain a completely logical construction of the circle which circumvents even the higher-inductive types.