そして微分形式だとなにが嬉しいか。接続を考えなくてよくなる。外微分の計算が超楽。なので、ライプニッツと体積形式の計算規則で計算中のテンソルが微分形式と外微分に寄せられるとうれしい。寄せられるかどうかの判断はどうするか？StringDiagramを使おう。

algebraicjulia.github.io/Cat… なんかstringdiagramが書けるjuliaパッケージが存在している…？

These kinds of diagrams always so satisfyingly tactile

StringDiagramタイプセット、TeXとTikzでなんとかするというのを諦めて、SVG図形をなんとかしてdraggableにして紐づけられた一行latexをmathjaxでSVG出力してネストさせ、トップレベルSVGをエクスポートできる静的ページとかそういう方向のほうがよさそう

ugh, I forgot to attribute. It's from Locatelli Nunes' PhD thesis

I really like the chart!

It's an adaptation of Marsden @StringDiagram and Nakahira's work. The lower wire is an expression in a locally small category C and the upper x wire is a hom-functor and the Phi is a generic functor C->Set. The semicircle on the right represents the identity as a set element, 1->C(x,x). The box on the functor wires is a natural transformation.

Ah, it might finally be my year to attend!

@viercc you'll like this, since it connects to why parametrised monads are endofunctor-enriched categories!

I've been experimenting with Idris implementations of free PROPs and free(ish) monoidal categories at the Monoidal Cafe. Would be happy to send a discord invite to anyone who wants to join in and chat about applications :D

Yeah: tikzit love patience is Nicola's recipe 😊

I remember seeing @NicolaPinzani do it; I think that’s made with tikzit and lots of love

Thanks for sharing!

I would be similarly delighted. Good to see more string diagrams out in the world.

This may be more convenient for capturing universal properties, as it is more symmetric than the kind/type/term interpretation. However, both approaches should generalise to arbitrary dimensions (either by giving each kind a type, or by introducing rewrites between rewrites).

There's another 2-dimensional approach to type theory, in which we view objects as types, 1-cells as terms, and 2-cells as rewrites between terms (cf. Seely's "Modelling computations: a 2-categorical framework").

By the way, I gave a talk last year with a similar motivation (i.e. "view kinds as objects, types as 1-cells, terms as 2-cells"). You can see the slides here: arkor.co/files/A 2-dimensi…. (I had intended to share my slides much earlier, but it just occurred to me that I never did.)

Beautiful #stringdiagram visualizer for cartesian closed categories, from the people who brought you Homotopy.io (Nick Hu, Alex Rice, and Calin Tataru). It can display and navigate very large terms, both in their textual and graphical form.😍 sdvisualiser.github.io/sd-vi…

Just received my copy

Got my copy just now! 🥳