module Data.These %access public export%default total data These a b = This a | That b | Both a b fromEither : Either a b -> These a bfromEither = either This That these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> cthese l r lr (This a)   = l athese l r lr (That b)   = r bthese l r lr (Both a b) = lr a b bimap : (f : a -> b) -> (g : c -> d) -> These a c -> These b dbimap f g (This a)   = This (f a)bimap f g (That b)   = That (g b)bimap f g (Both a b) = Both (f a) (g b) (Show a, Show b) => Show (These a b) where  showPrec d (This x)   = showCon d "This" $ showArg x  showPrec d (That x)   = showCon d "That" $ showArg x  showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y Functor (These a) where  map = bimap id mapFst : (f : a -> b) -> These a c -> These b cmapFst f = bimap f id bifold : Monoid m => These m m -> mbifold (This a)   = abifold (That b)   = bbifold (Both a b) = a <+> b bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> These a b -> f (These c d)bitraverse f g (This a)   = [| This (f a) |]bitraverse f g (That b)   = [| That (g b) |]bitraverse f g (Both a b) = [| Both (f a) (g b) |]