Thierry COQUAND - Logic and topology

The logic of topos is naturally described using intuitionistic higher-order logic, an intuitionistic version of a simple theory of types, a formal system designed by A. Church (1940). Two important axioms of this formal system are the axiom of extensionality and the axiom of description. Recently, Voevodsky formulated the axiom of univalence, which can be seen as a natural generalization of the axiom of extensionality, and showed that this axiom is valid in a model where a type is interpreted as a Kan simpl