Welcome to Opetopic!

Opetopic is an experimental graphical proof assistant for higher category theory.

The above diagram is a diagrammatic proof of the right unit law for morphisms in a higher category. For an explanation of what this means, see the documentation.