Higher Lenses

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.