> Было бы интересно узнать, чем бы тебе мог быть практически полезен Паша если бы у вас всё получилось.

вот это хороший вопрос. Задача Паши была сделать кодировку Черча (неприменимую в продакшине из-за неэффективности) для зависимой теории с построениями теормов индукции. Это невыполнимая задача, потому что в нашем ядре нет вообще ничего кроме чистой лямбды. Поэтому мы обогатили кодировку типов всеми необходимыми нам свойствами и скомпилировали терм индукции, который вычисляется как лимит тождественного функтора в категории алгберы заданного индуктивного типа. Другими словами построено равенство, модель теории категорий и на ней написали взятие лимитов, как микропрограмма для прошивки в чистой лямбде. Вот для этого и был нужен Паша.