The Category of Closed lenses
A closed lens is isomorphic to a container morphism.
Very importantly, they are in isomorphism with our previous definition of dependent lenses:
Lemma
Closed lenses are isomorphic to dependent lenses
We prove the isomorphism by providing map to and from dependent lenses.
public export
toClosed : a =%> b -> a =&> b
toClosed mor = !!
\x => mor.fwd x ## (\y => mor.bwd x y)
public export
fromClosed : a =&> b -> a =%> b
fromClosed (!! g) =
(\x => (g x).π1) <!
(\x, y => (g x).π2 y)
public export
closedIso : a =&> b ≅ (a =%> b)
closedIso = MkIso
fromClosed
toClosed
(\(x <! y) => Refl)
(\(!! fn) => cong (!!) (funExtDep $ \nx => sigmaProjId _))
This means that everything that worked before, works on closed lenses as well.
- relation with pointful lenses
- explain why we use this in practice (unifier likes matching on the first argument)