# Andrej Bauer: Impredicative encodings

Date of publication: 12. 5. 2014

Mathematics and theoretical computing seminar

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.

Vabljeni!