String-Diagramme

Matthias hat eine Art kleine (winzige) Bibliothek für String-Diagramme in Agda geschrieben. Das war nicht geplant, aber es hat so gut funktioniert, dass er gerne mit allen, die es interessiert, ein bisschen darüber reden würde.

Was sind String-Diagramme? Für mich sind String-Diagramme eine angenehme Notation für natürliche Transformationen zwischen Funktoren. (Oder allgemeiner für 2-Zellen zwischen 1-Zellen einer beliebigen 2-Kategorie.) Man zeichnet dabei Funktoren als senkrechte Linien (Strings) und natürliche Transformationen als Verzweigungspunkte. Damit kann man zum Beispiel extrem angenehm beweisen, dass jede Adjunktion eine Monade induziert.