自然変換
Menu Menu top : Agda による圏論入門 可換図 HomReasoning.agda 自然変換を理解すれば圏論は終わったようなものですが、さらっと可換とか書いてある割に良くわからないものです。そもそも自然変換とはなんなんのか? Agda を使うと理解できるようになるんでしょうか? 自然変換は二つの Functor : A -> B に対して定義されます。ということは、二つの圏A,B が関係しています。以下の図が可換になると簡単に説明されているのが普通です。 F(f) F(a) ---→ F(b) | | |t(a) |t(b) G(f)t(a) = t(b)F(f) | | v v G(a) ---→ G(b) G(f) これは、可換あるいは可換図の定義だと思うべきです。図は人用のもので、Agda にとっては、 等式 G(f)t(a) = t(b)F(f) だけが重要です。
Monad
A x N (N は計算量) Monad の例題 部分計算 計算には例外が付きものである。例外として未定値を返せる計算を考えよう。この時に、返す値は、通常返される値と、未定値のSum型になる。型変数を持つデータ構造は Functor だったのを思い出して、 data maybe {c : Level} (A : Set c) : Set c where just : A → maybe A nothing : maybe A Maybe : Functor Sets Sets Maybe = record { FObj = λ a → maybe a ; FMap = λ {a} {b} f → fmap f ; isFunctor = record { identity = extensionality {zero} ( λ x → ? ) ; distr = extensionalit
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
