Diagrams and Lean 4's Natural Transformations

Stream: general

[Dean Young]

Attached is a simple string diagram generator. I am interested in how such a thing could be "connected up" with Mathlib's Functor C D and NaturalTransform F G.

It would be really nice if there were a widget for string diagrams. One example could be the diagram here.

StringDiagramGenerator.py

[Adam Topaz]

Have you seen https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/String.20diagrams/near/421520311 ?

[Dean Young]

@Adam Topaz thanks for this!!

I was meaning to attend your talk but became very tired :-(