Lawful polymorphic optics

Assorted notes on lawful optics in the general, four-parameter form.

\begin{tikzcd} % https://q.deertopia.net/#q=WzAsNixbMCwwLCJTIl0sWzEsMCwiXFxtYXRoYmZ7Q30gXFxvdGltZXMgQSJdLFswLDEsIlQiXSxbMSwxLCJcXG1hdGhiZntDfSBcXG90aW1lcyBCIl0sWzIsMCwiQSJdLFsyLDEsIkIiXSxbMCwxLCJcXHRleHRybXt0b3B9IiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiYXJyb3doZWFkIn19fV0sWzIsMywiXFx0ZXh0cm17Ym90dG9tfSIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6ImFycm93aGVhZCJ9fX1dLFswLDIsIlxcbWF0aHJte292ZXJ9fmYiLDJdLFsxLDMsIjEgXFxvdGltZXMgZiJdLFsxLDQsIlxcbWF0aHJte3ByfV8yIl0sWzMsNSwiXFxtYXRocm17cHJ9XzIiLDJdLFs0LDUsImYiXV0= S & {\mathbf{C} \otimes A} & A \\ T & {\mathbf{C} \otimes B} & B \arrow["{\textrm{top}}", tail reversed, from=1-1, to=1-2] \arrow["{\mathrm{over}~f}"', from=1-1, to=2-1] \arrow["{\mathrm{pr}_2}", from=1-2, to=1-3] \arrow["{1 \otimes f}", from=1-2, to=2-2] \arrow["f", from=1-3, to=2-3] \arrow["{\textrm{bottom}}"', tail reversed, from=2-1, to=2-2] \arrow["{\mathrm{pr}_2}"', from=2-2, to=2-3] \end{tikzcd} ParseError: No such environment: tikzcd at position 7: \begin{̲t̲i̲k̲z̲c̲d̲}̲ % https://q.de…

\begin{tikzcd} % https://q.deertopia.net/#q=WzAsNixbMCwwLCJTIl0sWzEsMCwiXFxtYXRoYmZ7Q30gXFxvdGltZXMgQSJdLFswLDEsIlMiXSxbMSwxLCJcXG1hdGhiZntDfSBcXG90aW1lcyBBIl0sWzIsMCwiQSJdLFsyLDEsIkEiXSxbMCwxLCJcXHRleHRybXt0b3B9IiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoiYXJyb3doZWFkIn19fV0sWzIsMywiXFx0ZXh0cm17Ym90dG9tfSIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6ImFycm93aGVhZCJ9fX1dLFswLDIsIlxcbWF0aHJte292ZXJ9fmYiLDJdLFsxLDMsIjEgXFxvdGltZXMgZiJdLFsxLDQsIlxcbWF0aHJte3ByfV8yIl0sWzMsNSwiXFxtYXRocm17cHJ9XzIiLDJdLFs0LDUsImYiXV0= S & {\mathbf{C} \otimes A} & A \\ S & {\mathbf{C} \otimes A} & A \arrow["{\textrm{top}}", tail reversed, from=1-1, to=1-2] \arrow["{\mathrm{over}~f}"', from=1-1, to=2-1] \arrow["{\mathrm{pr}_2}", from=1-2, to=1-3] \arrow["{1 \otimes f}", from=1-2, to=2-2] \arrow["f", from=1-3, to=2-3] \arrow["{\textrm{bottom}}"', tail reversed, from=2-1, to=2-2] \arrow["{\mathrm{pr}_2}"', from=2-2, to=2-3] \end{tikzcd} ParseError: No such environment: tikzcd at position 7: \begin{̲t̲i̲k̲z̲c̲d̲}̲ % https://q.de…

\begin{tikzcd} % https://q.deertopia.net/#q=WzAsNSxbMCwxLCJTIFxcdGltZXMgUyJdLFswLDIsIkEgXFx0aW1lcyBTIl0sWzAsMywiUyJdLFswLDAsIlxcdG9wIFxcdGltZXMgXFx0b3AiXSxbMCw0LCJcXHRvcCJdLFswLDEsIlxcbWF0aHJte3ZpZXd9IFxcdGltZXMgMSJdLFsxLDIsIlxcbWF0aHJte3B1dH0iXSxbMywwLCJzIFxcdGltZXMgcyJdLFs0LDIsInMiLDJdXQ== {\top \times \top} \\ {S \times S} \\ {A \times S} \\ S \\ \top \arrow["{s \times s}", from=1-1, to=2-1] \arrow["{\mathrm{view} \times 1}", from=2-1, to=3-1] \arrow["{\mathrm{put}}", from=3-1, to=4-1] \arrow["s"', from=5-1, to=4-1] \end{tikzcd} ParseError: No such environment: tikzcd at position 7: \begin{̲t̲i̲k̲z̲c̲d̲}̲ % https://q.de…

References