decide :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide fx = case extract fx of
Left a -> Left $ either id (const a) <$> fx
Right b -> Right $ either (const b) id <$> fx

lightly edited from the final snippet here (which doesn't typecheck and might have a typo)

symm :: Either a b -> Either b a
symm = either Right Left
lcostrength :: Comonad f => f (Either a b) -> Either a (f b)
lcostrength fab = case extract fab of
Left a -> Left a
Right b -> Right $ const b <$> fab
rcostrength :: Comonad f => f (Either a b) -> Either (f a) b
rcostrength = symm . lcostrength . fmap symm
decide1 :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide1 = lcostrength . fmap rcostrength . duplicate
decide2 :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide2 = rcostrength . fmap lcostrength . duplicate
-- decide1 = decide2 =? decide

Can anyone see if the following definition:

lightly edited from the final snippet here (which doesn't typecheck and might have a typo)

Would be the same as the following definition(s):

`const b <$> fab`

be`either (const b) id <$> fab`

?After fixing the definition, the proof https://gist.github.com/Lysxia/11306596b08e2589a5a0dca9bf24b51a

It's honestly easier to prove with Coq than to think about whatever that means.

Also, the QuickCheck tests: https://gist.github.com/Lysxia/2394853edba387c3ba0fa8599e44a7be

@Lysxia Do you mean that

`const b <$> fab`

wouldn't typecheck or that it's wrong despite typechecking?I vaguely remember sticking all this in an ideone snippet before I posted here, so I think it typechecks

Also, thanks so much for working out a proof!

Oh, right. I get what's wrong with

`const b`

now. It'll overwrite stuff that we don't need to overwriteHmm, I'm increasingly suspicious that what I've labeled a strength isn't actually a strength

Although that discussion is probably more appropriate for #Category theory

nvm it's a strength