# Is Bool -> Maybe () isomorphic?

• A+
Category：Languages

I am trying to figure out, if `Bool -> Maybe ()` is isomorphic or not.

The possible combination are:

``True -> Just () True -> Nothing False -> Just () False -> Nothing ``

I would say, it is isomorphic and for every combination, it exists seperate functions to inverse it.

How to prove that the above morphism is isomorphic?

`Bool` and `Maybe ()` are isomorphic types (ignoring problems involving bottom), as witnessed by the following mappings between the two:

``b2m :: Bool -> Maybe () b2m True = Just () b2m False = Nothing  m2b :: Maybe () -> Bool m2b (Just ()) = True m2b Nothing = False ``

It is easy to verify that `b2m . m2b` and `m2b . b2m` are both equivalent to `id`:

``m2b . b2m \$ True == m2b (b2m True) == m2b (Just ()) == True == id True m2b . b2m \$ Fals == m2b (b2m False) ==  m2b Nothing == False == id False  b2m . m2b (Just ()) == b2m (m2b (Just ())) == b2m True == Just () == id (Just ()) b2m . m2b Nothing == b2m (m2b Nothing) == b2m False == Nothing == id Nothing ``

In your question, you don't have a single morphism. You have the building blocks for the 4 different functions that have type `Bool -> Maybe ()`, as follows:

``f1,f2,f3,f4 :: Bool -> Maybe () f1 True = Just () f1 False = Nothing  f2 True = Nothing f2 False = Just ()  f3 True = Just () f3 False = Just ()  f4 True = Nothing f4 False = Nothing ``

Likewise, there are 4 different functions of type `Maybe () -> Bool`:

``f5,f6,f7,f8 :: Maybe () -> Bool f5 (Just ()) = True f5 Nothing = False  f6 (Just ()) = False f6 Nothing = True  f7 (Just ()) = True f7 Nothing = True  f8 (Just ()) = False f8 Nothing = False ``

Some pairs of functions form an isomorphism, but some don't. The top of this answer shows that `f1` and `f5` do, but `f3` and `f8`, for example, do not.

``f3 . f8 \$ (Just ()) == f3 (f8 Just ()) == f3 False == Just () == id (Just ()) f3 . f8 \$ Nothing == f3 (f8 Nothing) == f3 False == Just () != id Nothing ``