Category of Lenses

Let $\mathcal{C}$ be a Cartesian Category. The category of lenses in $\mathcal{C}$ has the same objects as $\mathcal{C}\times\mathcal{C}$, and morphisms $(S,T)\to(A,B)$ consist of a "getter" $g:S\to A$, and a "setter" $s:S\times B\to T$.

This category can abstractly be constructed as the Total Category of the Fibrewise Opposite of the Simple Fibration of $\mathcal{C}$.

Properties

• A morphism $s:S\times B\to T$ over $g:S\to A$ is Cartesian if and only if $\langle\pi_{0},s\rangle:S\times B\to S\times T$ is Invertible.