Я скоро вам запрещу нетотальные языки обсуждать вообще :)

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

нет, не понятно. То что там написано очень похоже на ваш exists a. (a -> x, f a) <~> f x. А код который я скинул как раз требует Rank-N types, то есть логично предположить, что он как раз и нужен для экзистенциалов. И как раз эту идею и выражает.

предлагаю тогда в тишине помедитировать над статьями, над хаскельным типом койонеды

ок

и уточнить в другой группе, какие кванторы расставляет haskell неявно

Все беды Haskell от того, что они никак не могут договориться о стандартных расширениях.

вот сейчас дописал и расставил скобки, можете свериться

https://t.me/ru_catheory/9312

Можно все примеры на Clean переписать. Будет хотя бы однозначно. Думаете, имеет смысл использовать Clean в учебном пособии?

;-)
idris-ct: A Library to do Category Theory in Idris
Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Andre Knispel, Marco Perone, Erik Post, André Videla
https://arxiv.org/abs/1912.06191
We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.
idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory:
It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business.
Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.
#paper

Я за то, чтобы туториалы на агде писать

А какая от этого выгода?

Странно. Но ладно. А где исходники можно посмотреть?

Это да. Но не получается найти кусок о сетях Петри

а откуда ты exists взял?

тут сказано про лемму Йонеды, но есть еще и Койонеда
концы vs коконцы

вот ведь, нет?