fromLeft : (b -> a) -> Either a b -> a
fromRight : (a -> b) -> Either a b -> b
mapFstExtensional : ((x : a) -> f x = g x) -> (v : Either a c) -> mapFst f v = mapFst g v
mapSndExtensional : ((x : a) -> f x = g x) -> (v : Either w a) -> mapSnd f v = mapSnd g v
mapFstFusion : (v : Either a e) -> mapFst g (mapFst f v) = mapFst (g . f) v
mapSndFusion : (v : Either w a) -> mapSnd g (mapSnd f v) = mapSnd (g . f) v