Agda, теоркат и все все все
В развитие темы. Все знакомые уткнулись в PropositionalEquivalence. В рамках подготовки к объяснениям, написал про зависимые типы и Curry-Howard correspondence. What is enough type theory/agda for category theory? :)