  Bimorphic lenses are a simplification of polymorphic lenses that (like
polymorphic lenses) have a type defined by 4 parameters, but which are defined
in a monomorphic type system (i.e. an ordinary category with finite products).
We show that the category of bimorphic lenses is complete when the base
category is complete, cocomplete and cartesian closed, and so symmetric
bimorphic lenses can be defined as spans of ordinary bimorphic lenses. This is
in contrast to monomorphic lenses, which do not have pullbacks, and for which
the category of spans can be defined in an ad-hoc way only when the lenses
satisfy a certain axiom (the put-get law). This is a step towards a theory of
symmetric polymorphic lenses. Bimorphic lenses additionally play an essential
role in compositional game theory, and spans of bimorphic lenses are a step
towards a compact closed category of open games.
