AI 中文总结
研究严格笛卡尔对称幺半范畴上透镜的良好行为定律，定义带标签透镜，证明其构成严格对称幺半范畴及相关函子，观察组合蕴含关系确定定律充分条件。
AI 中文摘要
为了更好地理解严格笛卡尔对称幺半范畴上透镜的良好行为定律格局，我们定义了带标签透镜。我们证明带标签透镜构成一个严格对称幺半范畴，并配备一个到putget透镜范畴的严格对称幺半函子。然后我们观察了其他两个透镜定律的组合蕴含关系，分别将标签的变化依赖性和首尾依赖性确定为getput和putput的充分条件。
英文摘要
To better understand the landscape of well-behavedness laws for lenses on strict Cartesian symmetric monoidal categories, we define tagged lenses. We prove that tagged lenses form a strict symmetric monoidal category equipped with a strict symmetric monoidal functor into the category of putget lenses. We then observe compositional entailment for the other two lens laws, identifying change-dependence and first-last dependence of tags as sufficient conditions for getput and putput, respectively.
