Proposition [efr-UNIN]

Suppose \mathcal {M} is semicartesian---in other words, that I \in \mathcal {M} is terminal. Then there is a functor \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) \to \mathcal {C}, which takes a {A \choose X} to X, and pair \langle f: X \to M \cdot Y, g \rangle to the composite X \to M \cdot Y \to I \cdot Y \cong Y.

In the case of \mathsf {Optic}(\mathcal {M}), the map \mathsf {Optic}(\mathcal {M})({I \choose I}, {A \choose X}) \to \mathcal {M}(I,X) is a bijection.