Types - citations


The equivalence axiom and univalent models of type theory (2010)

I will show how to define, in any type system with dependent sums, products and Martin-Lof identity types,
the notion of a homotopy equivalence between two types
and how to formulate the Equivalence Axiom which provides a natural way to assert that ”two homotopy equivalent types are equal”.
I will speak about type systems. It is difficult for a mathematician since a type system is not a mathematical notion. I will spend a little time explaining how I see ”type systems” mathematically.
”Type systems” are formal deduction systems of particular ”flavor”.

Univalent Foundations Project (2010)

A few years ago I have come up with an idea for a new semantics for dependent type theories - the class of formal systems which are widely used in the theory of programming languages.


La théorie des types | Infini 24