Категорно комбинаторная машина

вся эта идея суперкомбинаторов

https://twitter.com/johncarlosbaez/status/1229449251261779977

О самой книге:

2-Dimensional Categories

Niles Johnson, Donald Yau

This book is an introduction to 2-categories and bicategories, assuming only the most elementary aspects of category theory. A review of basic category theory is followed by a systematic discussion of 2-/bicategories, pasting diagrams, lax functors, 2-/bilimits, the Duskin nerve, 2-nerve, adjunctions and monads in bicategories, 2-monads, biequivalences, the Bicategorical Yoneda Lemma, and the Coherence Theorem for bicategories. Grothendieck fibrations and the Grothendieck construction are discussed next, followed by tricategories, monoidal bicategories, the Gray tensor product, and double categories. Completely detailed proofs of several fundamental but hard-to-find results are presented for the first time. With exercises and plenty of motivation and explanation, this book is useful for both beginners and experts.

Что там интересного про теоркат?

если кто хочет им помочь, чтобы Agda Cubical прогонялась тестами автоматически

Наверное в завтипы лучше бросить

ok

Кстати. О теоркате. Где-то видел новость о proof assistant-е, основанном на сопряжениях. Но из головы вылетело название. Может быть, знает кто-нибудь о чём шла речь?

Только не на сопряжениях, а на концах-коконцах.
И наверное, это хаскель ;-)

Там было точно о сопряжениях. Даже помню слова об автоматическом их исчислении. Слышал от скалистов.