In verified generic programming, one cannot exploit the structure of concrete data types but has
to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads
are at the core of many applications of functional programming. This raises the question of what
useful ADTs for verified functors and monads could look like. The functorial map of many important
monads preserves extensional equality. For instance, if f , g : A...