khibino
クライスリ圏 / 表現可能関手 を Agda で形式化して、
米田の補題の証明を調べようと思います。
単純な関数の米田の補題だと、
forall x . (r -> x) -> f x ≅ f r
みたいな感じで、
右から左への変換で、
Haskell の単純な fmap が利用できます。
しかし、クライスリ圏が前提だと、
Rep x = r -> x (表現可能関手)
が、実質的に、
Rep x = r -> m x
なので、 Haskell でいう fmap ではなくなります。
具体的には、こんな感じの命題の証明を調べる予定です。
米田の補題の証明を調べようと思います。
単純な関数の米田の補題だと、
forall x . (r -> x) -> f x ≅ f r
みたいな感じで、
右から左への変換で、
Haskell の単純な fmap が利用できます。
しかし、クライスリ圏が前提だと、
Rep x = r -> x (表現可能関手)
が、実質的に、
Rep x = r -> m x
なので、 Haskell でいう fmap ではなくなります。
具体的には、こんな感じの命題の証明を調べる予定です。