right' ≡ dimap swapE swapE . left' where swapE :: Either a b -> Either b a swapE = either Right Left rmap Right ≡ lmap Right . right' lmap (left f) . right' ≡ rmap (left f) . right' right' . right' ≡ dimap unassocE assocE . right' where assocE :: Either (Either a b) c -> Either a (Either b c) assocE (Left (Left a)) = Left a assocE (Left (Right b)) = Right (Left b) assocE (Right c) = Right (Right c) unassocE :: Either a (Either b c) -> Either (Either a b) c unassocE (Left a) = Left (Left a) unassocE (Right (Left b)) = Left (Right b) unassocE (Right (Right c)) = Right c
unright ≡ unleft . dimap swapE swapE where swapE :: Either a b -> Either b a swapE = either Right Left rmap (either absurd id) ≡ unright . lmap (either absurd id) unsecond . rmap (first f) ≡ unsecond . lmap (first f) unright . unright ≡ unright . dimap unassocE assocE where assocE :: Either (Either a b) c -> Either a (Either b c) assocE (Left (Left a)) = Left a assocE (Left (Right b)) = Right (Left b) assocE (Right c) = Right (Right c) unassocE :: Either a (Either b c) -> Either (Either a b) c unassocE (Left a) = Left (Left a) unassocE (Right (Left b)) = Left (Right b) unassocE (Right (Right c)) = Right c