Есть такой парадокс Бурали-Форти (что это??) из теории множеств, который в принципе достаточно наглядно применим и к унивалентным основаниям математики UF/HoTT.
Когда мы переносим, например, алгебраические структуры между типами из разных вселенных, мы не можем их "свёртывать" автоматически, только через унивалентность -- требуется явный ручной перенос с проверкой инвариантов. Мы не можем залифтить условный моноид из Set 0 до Set 1 с помощью унивалентности из-за теоретических ограничений...

Совсем на пальцах: в ООП у нас есть классы и метаклассы (или тайпклассы в ФП, откуда мы попадаем в existential types :), потому что мы не можем создать "класс всех классов" без парадоксов (в Java нельзя унаследоваться от List<String>).

Или когда мы создаём некоторый модуль как расширение существующей системы (условный плагин), для управления плагинами нам обязательно потребуется PluginManager -- мета-плагин. Но он не может быть "плагином всех плагинов", потому что в таком случае ему потребуется в частности управлять самим собой, что ведёт к самореференции и циклическим зависимостям.

Плагины ≠ система управления плагинами! (так же, как тип ≠ вселенная типов)

База: проектируем систему математически, с эксплицитным разделением уровней !

Менеджер должен существовать на мета-уровне, не смешиваясь с объектами, которыми он управляет.
Сервис, который должен контролировать сервисы, требует нового явного, осознанно вводимого уровеня абстракции; не надо пытаться запихнуть мета-функциональность в тот же слой.

Подробнее разберём и это, и многое другое, в гайде "Функциональные архитектуры".