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”.
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.