Oℕ
В Хотт можно построить категорию Cat без рили белив ми
В формулировке категории используется встроенное равенство = индексированный индуктивный тип с одним конструктором, а не сетоид. Его замечательно использовать, однако построить его обычно сложно. Поэтому во всех нетривиальных случаях пишется вот это
https://github.com/statebox/idris-ct/blob/master/src/Basic/Functor.lidr#L165
