...В мировой микро-тусовке по hott-"программированию" (считанные десятки человек) пишут что-то подобное в основном на хаскеле, ну а я сделал на питончике 🙈

Причём у них там будешь называться реально чётким пацаном, если

a) не просто такое реализуешь, а сделаешь "свой солвер" никому нафиг не нужный , и

б) обязательно добавить кубик (это вообще чисто понтовый топчик).
(пять лет назад я пояснял что это: "Кубическая теория типов для малышей") - только тогда будешь считаться cs-просветлённым 🙏

Впрочем, до этой тусовки мне нет абсолютно никакого дела. Буду продолжать эти темки исключительно на русском, и только в рунете (жаль сайт hott ру занят какой-то попсой :).
Хотя кубик будет обязательно.

так-то я больше склоняюсь к тому, чтобы сделать - по теории типов с нуля до хотт и далее - обучающую гача-игру в духе genshin impact 😬
плавно повышать свой уровень универсума, автоматически получая доступ ко всё более сложным конструкциям.

Хотя нет... В хотт 5+ уровень - это уже наверное на премию Филдса 😇
формализация (∞,1)-топосов, моделирование высших группоидов, бесконечно-категорные структуры...

А в генше вроде до сотого левела можно...

С другой стороны, каждый универсум легко бьётся минимум на десяток подуровней для изучения, и для первых двух-трёх универсумов темп прохождения изучения получается примерно как в GI 💎

(продолжение следует)