双晶透镜的极限
Limits of bimorphic lenses
摘要：
双形态透镜是多形态透镜的简化，其（像多形态透镜）具有由4个参数定义的类型，但是其在单形态类型系统（即，具有有限乘积的普通类别）中定义。我们证明了当基范畴完备、上完备和闭时，双态透镜范畴是完备的，因此对称双态透镜可以定义为普通双态透镜的跨距。这与单形透镜相反，单形透镜没有拉回，并且只有当透镜满足一定公理（放-得定律）时，才能以特定的方式定义跨度的类别。这是朝向对称多形透镜理论的一步。双态透镜在组合对策论中也起着重要的作用，双态透镜的跨度是迈向开放游戏的紧凑封闭类别的一步。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
