Prop structures

Stream: Is there code for X?

[Alex Meiburg]

Is there anything in Mathlib for the unforunately named "Prop" structure? In the sense of https://en.wikipedia.org/wiki/PROP_(category_theory) . It's a nice way of algebraically describing quantum circuits, and I would like to integrate with a such description if one exists.

It is, as you might imagine, an utterly unsearchable name in Lean :P

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Categorical.20tensor.20power