Theory Lenses_And_Other_Optics.Focus
theory Focus
imports Lens Prism
begin
section‹Foci›
text‹A focus is a common generalization of focuses and prisms. With focuses roughly corresponding
to quotients and prisms to subsets, a focus can be seen as a way of representing a subquotient.
Typically, foci do not arise directly, but rather as the composition of (the liftings to foci of)
focuses and prisms.
Note that one could also use the type \<^typ>‹('a ⇒ 'a) ⇒ ('s ⇒ 's option)› in the type of the
modification function, here, allowing the ``lifted'' function to return \<^term>‹None› on values
outside of the domain the view. Here, we instead expect (and axiomatize below) that the modification
function is simply the identity on those inputs:›