Skip to content

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

Notifications You must be signed in to change notification settings

dignissimus/Untangle

Repository files navigation

Untangle

Untangle is a Lean4 widget that displays string diagrams for morphisms inside categories and allows you to rewrite expressions by clicking on natural transformations and morphisms in the string diagram.

This widget currently has rewrite rules for Monads. Next, I'd like to add rules for symmetric monoidal categories and bimonoids/Hopf algebras.

Video demonstration

https://youtu.be/mLCrU9-1jko

Image

image

Example usage

Open the Example.lean file and follow the instructions

Notes

  • This proof of concept is work in progress and is not yet ready for general purpose use.

About

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published