3 problems

Wiring-diagram multicategory conjecture. The multicategory of wiring diagrams is precisely the produoidal category of lenses once dependencies are no longer tracked explicitly.

Let $\cC$ be a category. Write $\mathbf{Lens_{Cart}}(\cC)$ for the category of cartesian lenses and $\mathbf{Optic}(\cC)$ for the category of optics. Let…

Dependent-lens diagram conjecture. Dependent lenses in ${\mathcal C}$ fit in a similar diagram to the one described for lenses and dependent optics.