Рефакторинг -- это трансформация унаследованного (по определению) кода без изменения его функциональности.

Если посмотреть на такую трансформацию через линзу HoTT, то это будет, по сути, умение видеть (понимание) эквивалентности между различными парадигмами полиморфизма.

1. Параметрический полиморфизм -- это база универсальности.

Функция
map (f: 'a -> 'b) (list: 'a list) : 'b list
работает единообразно для любых типов a и b. Нам не нужно (да и невозможно) "заглядывать" внутрь a.

Это гомотопия (непрерывное преобразование), гомотопическая инвариантность.

Тип forall a b. (a -> b) -> List a -> List b -- это пространство всех возможных реализаций (всех функций с данным типом, и все они гомотопически эквивалентны).

Такая программа будет постоянной на эквивалентных типах: она не может делать странных вещей, зависящих от конкретного типа (для строк -- удваивать, а для чисел -- извлекать корень), из чего гарантируется её универсальность.

Параметрический полиморфизм -- это "контракт", который гарантирует, что полиморфная функция универсальна.