The squares
are pullbacks in any category with products, even if it does not admit pullbacks in general.
It follows that the full subcategory of \mathcal {C}^\to spanned by objects of this form is always a fibration over \mathcal {C}, which is isomorphic to \mathsf {coOptic}(\mathcal {C})---the fiberwise dual is isomorphic to \mathsf {Lens}(\mathcal {C}).
