generated at
Hask圏の関手圏と自然同型
Hask圏の関手圏Funと自然同型


関手圏\mathrm{Hask}^\mathrm{Hask}


自然同型
上図の他のものを見る
hs
alpha :: Maybe a -> Either () a alpha Nothing = Left () alpha (Just x) = Right x beta :: Either () a -> Maybe a beta (Left ()) = Nothing beta (Right x) = Just x
beta は alpha の逆射になっている
hs
beta.alpha == id_maybe alpha.beta == id_either
alpha 、 beta は多相的な関数なので、自然変換である
これらは同型である自然変換なので、Maybe, Eitherにおける自然同型である



「自然同型」というものが、「2つの関手が本質的に同じ」であることを示すのであれば、上の議論から
Maybe a と Either () a は本質的に何の違いもない、ということが言える
a に Int を代入するなら
正規の値の方は例えば
hs
Just 100 Right 100
失敗の値の方は
hs
Nothing Left ()
と、なる
これらを同じものとみなせば、関手自体を全く同じものと見なすことができる



参考
『圏論入門』 p.47