Andrej Bauer: Impredicative encodings

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!