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?
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
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
f5 do, but
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