一句话：在 HoTT/单价基础中提出高阶透镜，解决传统良行为透镜在证明相关设置下失效的问题，并刻画其性质。
论文指出，在同伦类型论与单价基础下，若证明相关地处理全函数且非常良行为的透镜（lens），传统透镜定义会失去良好性质。作者提出高阶透镜（higher lens）：它包含源类型与“视图类型×剩余类型”之间的等价，以及从剩余类型到视图类型命题截断的函数；也可等价表述为 getter 函数，并证明其纤维族是相干常值的，即通过命题截断分解。作者研究其性质：在满足同一性证明唯一性（UIP）的类型上，高阶透镜与传统透镜等价；并利用相干常值函数的余归纳刻画，证明高阶透镜对 n-截断类型也是 n-截断的。
We show that total, very well-behaved lenses are not very well-behaved when treated proof-relevantly in the setting of homotopy type theory/univalent foundations. In their place we propose something more well-behaved: higher lenses. Such a lens contains an equivalence between the lens's source type and the product of its view type and a remainder type, plus a function from the remainder type to the propositional truncation of the view type. It can equivalently be formulated as a getter function and a proof that its family of fibres is coherently constant, i.e. factors through propositional truncation.We explore the properties of higher lenses. For instance, we prove that higher lenses are equivalent to traditional ones for types that satisfy the principle of uniqueness of identity proofs. We also prove that higher lenses are n-truncated for n-truncated types, using a coinductive characterisation of coherently constant functions.
DOI 原文 ·
@inproceedings{paperbot6248,
title = {Higher Lenses},
author = {Paolo Capriotti and Nils Anders Danielsson and Andrea Vezzosi},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470613}
}