Conversion.idr

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.

export 0
clsEqToDLensEq : ClosedEq m n SigEq -> fromClosed m <%≡%> fromClosed n
clsEqToDLensEq eq = rewrite clsEqToEq SigEq sigEqToEq eq in reflexive
 
export 0
clsEqToDLensEq' : ClosedEq (toClosed m) (toClosed n) SigEq -> m <%≡%> n
-- clsEqToDLensEq' eq = rewrite clsEqToEq SigEq sigEqToEq eq in reflexive
 
export 0
clsEqToPropEq : ClosedEq (toClosed m) (toClosed n) SigEqS -> m === n