[Выворот мозга] общий подход к infix-операторам

До изучения HoTT я думал, что цепная математическая запись a = b = c крайне удобный способ записывать (a = b) ∧ (b = c), потому что использование цепочки из n знаков равенства вместо подробного расписывания экономит O(n) символов.

Сейчас я считаю, что это крайне удобный способ записывать (q: a = b, p: b = c, q = p), потому что он экономит O(n^2) символов.

* * *
Обычно для infix-операторов в языках программирования приходится указывать что они лево-ассоциирующие или право-ассоциирующие, что во-первых некрасиво когда оператор ассоциативный и таким образом одинаково ведёт себя, что там ни напиши, а во-вторых исключает возможность нативно поддерживать такие вот штуки как a = b = c выше.

Про такие infix-операторы хочется указывать не левость-правость, а декларировать, к какой она относится категории (возможно высшей и/или обогащённой) или слабой подкатегории таковой. Для _=_: {T: Type} (T, T) => Type это высшая категория Id, Для _≤_: (Real, Real) => Prop это порядок на вещественных числах (взятый как категория, в частности Prop-категория), _≤_ это соответственно слабая без подкатегория таковой, для метафонтовского _–[_]–_ (Point, Properties, Point) => Polyline это Polyline-категория ломаных Безье. Ну а так как любое множество с ассоциативной операцией можно достроить до моноида добавлением одной точки, всякий ассоциативный оператор _+_: (A, A) => A представляется стрелкой слабой подкатегории (А, +)-категории с одним объектом.

(А ещё, если целевая n-категория ещё и n-tupled, то можно не просто по-цепочке значки рисовать, а в произвольную коммутативную диаграмму оформлять.)