Formalizing functional analysis structures in dependent type theory

This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topol-ogy and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical analysis, for the Coq proof assistant. It extends the Mathematical Components library, geared towards algebra, with topics in analysis. This marriage arouses issues of a more general nature, related to the inheritance of poorer structures from richer ones. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.