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