Definition Simple Bimorphic Lens [lcc-0001]

Let \mathcal {C} be a Cartesian monoidal category. Then \mathsf {Lens}(\mathcal {C}) is the category whose objects are pairs \binom {X}{A} of objects in \mathcal {C}, where morphisms are defined by \operatorname {\mathrm {Hom}}\left (\binom {X}{A}, \binom {Y}{B}\right ) = \mathcal {C}(X,Y) \times \mathcal {C}(X \times B, A), and where composition is defined by (f^+: X \to Y, f^-: X \times B \to A) ; (g^+: Y \to Z, g^-: Y \times C \to B) \\= (f^+;g^+, (x,c) \mapsto f^-(x,g^-(f^+(x),c))) (The expression of the composite of the backwards passes in terms of elements is easily seen to correspond to a composite of maps between products in a generic Cartesian category)