Okay, that’s a reasonable ask. In that case, you need the three lens laws (aka. the very well-behaved lens laws): GetPut, PutGet, and PutPut.
-- Suppose there is a lens
get :: s -> a
put :: s -> a -> s
-- satisfying the three laws
GetPut :: forall s. put s (get s) = s
PutGet :: forall s a. get (put s a) = a
PutPut :: forall s a b. put (put s a) b = put s b
Let us recall the definition of the candidate isomorphism:
to :: s -> (a, a -> s)
to s = (get s, put s)
from :: (a, a -> s)
from (a, f) = f a
If we restrict the complement (a -> s) to exactly the subset of functions that can be obtained by put, we can show that (to, from) is an isomorphism. In set comprehension notation:
-- aka. the *image* of put
c = {f :: a -> s | exists s. f = put s}
GetPut proves the roundtrip from s to (a, c) and back.
from (to s) = put s (get s) = s
For the other roundtrip, we start with a pair (a, c), where c is from the image of put. So we actually start with a pair (a, put s).
The from then to roundtrip goes:
to (from (a, put s)) = (get (put s a), put (put s a))
The first component simplifies by PutGet.
get (put s a) = a
The second component simplifies by an eta-reduced reformulation of PutPut:
put (put s a) = put s
Putting these steps together, the from-then-to roundtrip:
to (from (a, put s)) = (a, put s)
Conclusion: to and from form an isomorphism between s and (a, c) where c = {f :: a -> s | exists s. f = put s}.
to . from = id
from . to = id
To show that PutPut is necessary to get an isomorphism, here is a counterexample with a lens that does not satisfy it. Let s be a type with three elements A | B | C, and a be Bool (two elements).
get :: s -> a
get A = True
get B = False
get C = False
put :: s -> a -> s
put _ True = A
put A False = B
put B False = B
put C False = C
It satisfies GetPut and PutGet, but there is no isomorphism between A | B | C and (Bool, c) for any c because 2 does not divide 3.