Category module に関して
Menu MenuAgda と圏論
Agda で圏論を勉強している人はたくさんいるでしょう。そのうちのいくつかは github などで公開されています。ここでは、石井ひろみ氏による
https://github.com/konn/category-agda を使います。
https://github.com/copumpkin/categories も良いのですが、最初に見つけたのが前者だったので。
圏論は勉強するとキリがありませんが、ここでは、
＊ 自然変換の定義＊ 圏のMonadの定義＊ Haskell の Monad の元の Kleisli 圏の射の結合則の証明
をとりあえずの目標にします。Agda で Cagegory の定義を除いて、700 行程度。
さらに、
＊ 随伴関手から、Universal mapping の解を導く＊ Universal mapping の解法から随伴関手を導く
と、さらに先の目標として、
＊ Monad を随伴関手から導く＊ Kleisli 圏による Monad の Resolution ( 随伴関手の導出)＊ Kleisli 圏に対する Comparison Functor ＊ Eleinberg-Moore 圏による Monad の Resolution ( 随伴関手の導出)＊ Eleinberg-Moore 圏に対する Comparison Functor
＊ Yonda Functor ＊ Limit に関するいくつかの性質 (離散圏など)＊ フロイトの随伴函手定理 ( コンマ圏など )＊ Applicative Functor と Monodial Functor の同等性
を目指します。Agda で1万行程度になります。
Limiti とか Equlizer がないのがちょっと足りないけど、気が向いたら足すでしょう。
ここでは、Category module を少し見てみます。
Agda module library の設定
Agda のlibrary は、~/.agda で指定します。
~/.agda/defaults にはライブラリの名前、
standard-library
category-agda
~/.agda/libraries には絶対パスを書きます。
/usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
/Users/kono/src/public/category-agda/category-agda.agda-lib
古い Category module の設定
Agda の Library は適切な場所に置き、Emacs の customise で指定してました。
Agda mode から
M-X customise-mode
ここで、
Agda2 Include Dirs: [Hide Value]
[INS] [DEL] Directory: .
[INS]
[State]: SAVED and set.
に[INS]で指定します。
[Set for Current Session] [Save for Future Sessions]
です。.emacs に直接、
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(agda2-include-dirs (quote ("." "/Users/kono/src/public/category-agda")))
'(gud-gdb-command-name "gdb --annotate=1")
'(large-file-warning-threshold nil)
'(viper-ESC-keyseq-timeout 0)
'(viper-toggle-key [(control 121)]))
と書く方が簡単かも知れません。
Category module の構成
top level に Category.agda があり、そこに圏の定義が書いてあります。 record で書いたように、圏の公理が record の中に書いてあるという形式です。93行と短いですが、Agda なのであなどれません。Category directory 以下に、実際に構成した圏があります。ここで使うのは Cat.agda つまり圏の圏のみです。Identity Functor や Functor の合成が Cat.agda に記述されています。
Category.agda
Category.agda 圏の簡単な入門は、Category を見てもらうと良いと思います。重要なのは Object (対象)と、Object 間の Hom ( Homomorphism / 射 ) 定義です。公理自体は式でしかないが、Object と Hom が何物なのかを理解しないと操作できません。
IsCategory という record に圏の公理が記述されています。
record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁)
(Hom : Obj → Obj → Set c₂)
(_≈_ : {A B : Obj} → Rel (Hom A B) ℓ)
(_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
(Id : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
field
isEquivalence : {A B : Obj} → IsEquivalence {c₂} {ℓ} {Hom A B} _≈_
identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f
identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f
o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
associative : {A B C D : Obj} {f : Hom C D} {g : Hom B C} {h : Hom A B}
→ (f o (g o h)) ≈ ((f o g) o h)
Obj と Hom はそれぞれ Set c₁ と Set c₂ という集合です。Hom には引数が二つあります。Domain と Codomain 、つまり、元のObjのSet(入力の型(集合))と行き先の Obj のSet 値域です。それぞれに別な集合の Level が割り当てられています。
Hom は写像に相当しますが、写像そのもの (Obj -> Obj) ではなくて、写像の集合だというわけです。その中の一つが実際の射 (写像 )です。これらは ( 後で説明する別な record を通して) 、
a b : Obj A
f g : Hom A a b
という形で使います。a b が Obj で、f g は a から b への射というわけです。Hom A a b は、a から b への射の全体を表す集合です。
(_≈_ : {A B : Obj} → Rel (Hom A B) ℓ)
は射の等号です。Rel は Relation.Binary.Core に定義されていて、
-- Heterogeneous binary relations
REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ
-- Homogeneous binary relations
Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = REL A A ℓ
と定義されています。Rel は集合で Level として a ⊔ suc ℓ を持っています。ここでの集合は、例えば、前に作成した、
data _==_ {A : Set } : List A -> List A -> Set where
reflection : {x : List A} -> x == x
とかが来ることが期待されいますが、何が来るかは、ここでは指定していません。抽象的な圏は等号がありさせすれば良くて、その具体的な実現とは関係ないわけです。
(_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
が、射の合成です。ここで指定されているのは合成の型だけです。ここでも実体はありません。
最後に、
(Id : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
自己射である Id (の型)が定義されています。ここで一つ集合のレベルが上がっているのは、Hom が Set (a ⊔ suc ℓ) だからです。
Obj 、Hom、射の等号、射の合成、そして射の単位元、この5つで圏の定義に含まれる要素のすべてです。
圏の公理
圏の公理も5つしかありません。
isEquivalence : {A B : Obj} → IsEquivalence {c₂} {ℓ} {Hom A B} _≈_
identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f
identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f
o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
associative : {A B C D : Obj} {f : Hom C D} {g : Hom B C} {h : Hom A B}
→ (f o (g o h)) ≈ ((f o g) o h)
最初の IsEquivalence は、やはり、 Relation.Binary.Core に定義されていて、
-- Equivalence relations
-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.
record IsEquivalence {a ℓ} {A : Set a}
(_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
field
refl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_
reflexive : Dummy._≡_ ⇒ _≈_
reflexive Dummy.refl = refl
となっています。これらは、そこに、
-- Reflexivity of _∼_ can be expressed as _≈_ ⇒ _∼_, for some
-- underlying equality _≈_. However, the following variant is often
-- easier to use.
Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x
-- Generalised symmetry.
Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
REL A B ℓ₁ → REL B A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q
Symmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_
-- Generalised transitivity.
Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_
と定義されています。これらの公理を集めた record が IsEquivalence なわけです。これらの公理はいつでも呼び出すことができます。∼ は、 Reflexive _≈_ とかで呼び出す時に ≈ に置き換えられていることになります。
Reflexive _∼_ = ∀ {x} → x ∼ x
は x ≈ x ですが、data で記述されているわけではないので、パターンマッチとして使うことはできません。
Sym に出てくる flip は Function.agda に
flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y
とあります。引数の順序を変えているだけです。つまり、x ≈ y -> y ≈ x です。
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
は、
x ≈ y -> y ≈ z -> x ≈ z
です。
射の Equivalence の制限
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
が Relation.Binary.Core にありますが、これは直接に使わないように工夫されているようです(なのでSetでない対象を持つ圏も扱える)。その工夫に従って証明していきます。具体的には、射の等号では、
☓ cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } →
☓ B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b
☓ cong-≈ eq f = ?
がありません。これは、本来は、
☓ cong-≈ refl f = reflという形の証明を持つはずなのですが、_≈_ は data として定義されていないので、これを証明することができません。(できるのかも知れないけど、僕はできませんでした)
≡ から ≈ を導くことは可能です。
-- How to prove this?
≡-≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y
≡-≈ refl = refl-hom
≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } →
a ≡ b → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b
≡-cong refl f = ≡-≈ refl
しかし、逆はできません。
☓ ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y
☓ ≈-≡ x≈y = ?
自分で作る圏の公理として導入することは可能です。
経験的に cong 抜きで、ほとんどの証明が可能ですが、それが圏の要請なのかどうかは良くわかりません。
cong の代わりに使えるのは、o-resp です。
o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
確かに cong に似ています。関数の代わりに h g という等しい射を付加することができます。この公理は圏論の本で記述されていることは、ほとんどありません。おそらく、cong を仮定するからでしょう。
Identity と結合則
identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f
identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f
Id は型しか規定されていなかったので、実際に Identity として使えることを示すのが、この公理です。等式を生成するように使用します。
associative : {A B C D : Obj} {f : Hom C D} {g : Hom B C} {h : Hom A B}
→ (f o (g o h)) ≈ ((f o g) o h)
が結合則を表しています。面倒なのは、
{f : Hom C D} {g : Hom B C} {h : Hom A B}
この順番です。
f は C から D への射 (arrow)、左から右
ですが、結合は、
f o g = \x -> f ( g ( x ) )
つまり、右から左。x は A から始まるので、後ろの方から h : A -> B, g : B -> C, f : C -> D とします。
しかし、{h : Hom A B} {g : Hom B C} {f : Hom C D} という順番にするのは式に出てくる順序と暗黙の引数の順序が異なるのでよろしくありません。
日本語的に、
x を f してから g する
f o g = \x -> ( ( x ) f ) g
とすれば結合も、左から右になって、
nihon-associative : {A B C D : Obj} {f : Hom A B} {g : Hom B C} {h : Hom C D}
→ (f * (g * h)) ≈ ((f * g) * h)
となったのでしょうけどね。Forth や PostScript という言語では、こういう後置記法が採用されています。それなりに便利ですが、あまり広まりませんでした。
圏の Constructor
IsCategory は圏の公理だけを記述しています。実際に圏を構成する場合は、以下の record を使います。
record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
infixr 9 _o_
infix 4 _≈_
field
Obj : Set c₁
Hom : Obj → Obj → Set c₂
_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C
_≈_ : {A B : Obj} → Rel (Hom A B) ℓ
Id : {A : Obj} → Hom A A
isCategory : IsCategory Obj Hom _≈_ _o_ Id
dom : {A B : Obj} → Hom A B → Obj
dom {A} _ = A
cod : {A B : Obj} → Hom A B → Obj
cod {B = B} _ = B
ちょっと省略しています。このように二段の record で数学的なものを表現するのが定番の方法のようです。Category は Constructor で、IsCategory が性質を表したものだということでしょう。infix などの優先順位はこちらに書きます。Obj や Hom は二度同じ物を書くことになります。しかし、これにょり、Obj や Hom にアクセスしやすくなります。
field だけでなく、関数もも記述することができます。中で、Obj などを呼び出すことができます。これは、オブジェクトのインスタンスメソッドと同じ働きをします。dom と cod は、射の元の Obj と行き先のObj を取り出すメソッドです。暗黙の入力変数を推論させて、推論した値を返す方法で、引数の中身を取り出しています。Hom が record ならば、record 経由で取り出すことができますが、この定義では「Hom が何か」をはっきりとは決めてないので、このような方法になります。
field 定義の中でも field を呼び出すことができますが、物理的に前の行で前もって定義されていることが必要です。つまり、field の順序を勝手に変えることはできません。関数の方は where などを使って順序を工夫することができます。
Category record は、もちろん field を指定して作ることもできますが、「とにかく、何かの Category がある仮定する」ことができます。 category-ex.agda
open import Level
open import Category
postulate c₁ c₂ ℓ : Level
postulate A : Category c₁ c₂ ℓ
これで、待望の「純粋に抽象的な Cateogry 」が Agda の中で手に入りました。対象と射は以下のようにします。
postulate a b : Obj A
postulate f g : Hom A a b
Obj は record の field なので、引数として Category A の A を取っています。つまり、「 method object 」というメソッド呼び出しに相当します。Agda は mononorphic なので、メソッド名( = record の field 名 ) は、他と重なることはできません。同時に開けなければ重なってもかまいせんが、同時に使う場合には、module 呼び出し時に名前を変えるなどの工夫が必要となります。
射の式
次に射の結合をしたいわけですが、_o_ は、record の field なので、
_o_ A f g
と書く必要があります。
b != a of type (Category.Category.Obj A)というエラーが出ます。 Hom を結合するためには、a -> b, b -> c でなければなりません。
postulate a b c : Obj A
postulate g : Hom A a b
postulate f : Hom A b c
open Category.Category
h = _o_ A f g
これで結合ができました。でも、せっかく、 _o_ は infix にしたのに、これでは残念な感じです。Category.agda では、三項演算子を使っています。
_[_≈_] : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → {A B : Obj C} → Rel (Hom C A B) ℓ
C [ f ≈ g ] = Category._≈_ C f g
_[_o_] : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
C [ f o g ] = Category._o_ C f g
なるほど。
i = A [ f o g ]
となります。
Functor の定義
Functor も同じように二段階の record で定義されています。
record IsFunctor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁′ c₂′ ℓ′)
(FObj : Obj C → Obj D)
(FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B))
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
field
≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ]
identity : {A : Obj C} → D [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {D} (FObj A)) ]
distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
→ D [ FMap (C [ g o f ]) ≈ (D [ FMap g o FMap f ] )]
record Functor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′)
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
field
FObj : Obj domain → Obj codomain
FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
isFunctor : IsFunctor domain codomain FObj FMap
関手 (Functor )は、対象の写像 FObj と、射の写像 FMap を持っています。そして、分配法則と単元の保存が射について定義されています。射の cong はないので、代わりに ≈-cong があるというわけです。
{_} は暗黙の引数の位置を確定するために使っています。Functor は射を扱うので集合の Level が一つ上がっています。
射の式が入れ子になるたびに D [ ] と書かなければなりません。Agda では、どこに空白を入れるかは重要ですが、() だけは空白を入れずに書くことができます。しかし、[] は、そうはいきません。必ず、空白が必要です。
この分配法則を呼び出すには、以下のようにします。
--T(g f) = T(g) T(f)
open Functor
Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
→ A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
Lemma1 = \t → IsFunctor.distr ( isFunctor t )
open Functor したので isFunctor を使えて、open IsFunctor してないので、IsFunctor.distr と record を明示した中途半端な呼び出しですが、これが便利なようです。
これが圏論での最初の証明(公理である)です。射の等式があり、証明として、IsFunctor.distr ( isFunctor t ) があります。AとかTとかの圏や関手は入力変数として仮定されています。これらは、暗黙の引数であり、
A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
の隠れた仮定になっています。圏の教科書に載っている
T(g f) = T(g) T(f)
を上のように翻訳すれば良いわけです。
関手は圏から圏への射なので、異なる圏二つが出てくる場合もあります。その場合には A とか B とかを丁寧に指定することになります。A や B を暗黙の引数にして推論させることもできますが、Agda が非常に重くなります。
Haskell では Functor は fmap :: ( a -> b ) -> ( t a -> t b ) という型を持ちますが、ここでは射から射を得る型になっています。
FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
圏の例
Category はある意味ではありふれたものです。ここでは三種類の見慣れたものが Category であることを示しましょう。
圏としての List と Monoid 最初の例は List です。既に結合則を証明しています。
infixr 40 _::_
data List (A : Set ) : Set where
[] : List A
_::_ : A -> List A -> List A
infixl 30 _++_
_++_ : {A : Set } -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
data ListObj : Set where
* : ListObj
List の対象はただ一つの要素からなる集合です。ここでは data として作っています。_++_ が List の圏の射の演算です。
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
≡-cong = Relation.Binary.PropositionalEquality.cong
isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ []
isListCategory A = record { isEquivalence = isEquivalence1 {A}
; identityL = list-id-l
; identityR = list-id-r
; o-resp-≈ = o-resp-≈ {A}
; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
}
where
list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x
list-id-l {_} {_} = refl
list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x
list-id-r {_} {[]} = refl
list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} )
list-assoc : {A : Set} -> { xs ys zs : List A } ->
( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
list-assoc {_} {[]} {_} {_} = refl
list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y )
( list-assoc {A} {xs} {ys} {zs} )
o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } →
f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
o-resp-≈ {A} refl refl = refl
isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_
isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
record { refl = refl
; sym = sym
; trans = trans
}
ListCategory : (A : Set) -> Category _ _ _
ListCategory A =
record { Obj = ListObj
; Hom = \a b -> List A
; _o_ = _++_
; _≈_ = _≡_
; Id = []
; isCategory = ( isListCategory A )
}
圏の性質は、List が満たす定理として証明していきます。
もう一つの例は Monoid です。Monoid は結合則と単位元を持つただ一つの演算を持つ代数です。
やはりただ一つの要素からなる対象を持ちます。これは data を作って作ります。
open import Algebra.Structures
open import Algebra.FunctionProperties using (Op₁; Op₂)
data MonoidObj : Set c where
! : MonoidObj
record ≡-Monoid c : Set (suc c) where
infixl 7 _∙_
field
Carrier : Set c
_∙_ : Op₂ Carrier
ε : Carrier
isMonoid : IsMonoid _≡_ _∙_ ε
open ≡-Monoid
open import Data.Product
isMonoidCategory : (M : ≡-Monoid c) -> IsCategory MonoidObj (\a b -> Carrier M ) _≡_ (_∙_ M) (ε M)
isMonoidCategory M = record { isEquivalence = isEquivalence1 {M}
; identityL = \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
; identityR = \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
; o-resp-≈ = o-resp-≈ {M}
}
where
o-resp-≈ : {M : ≡-Monoid c} -> {f g : Carrier M } → {h i : Carrier M } →
f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
o-resp-≈ {A} refl refl = refl
isEquivalence1 : {M : ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M } _≡_
isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
record { refl = refl
; sym = sym
; trans = trans
}
MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
MonoidCategory M =
record { Obj = MonoidObj
; Hom = \a b -> Carrier M
; _o_ = _∙_ M
; _≈_ = _≡_
; Id = ε M
; isCategory = ( isMonoidCategory M )
}
圏の性質は、Monoid の性質そのものです。List は Free Monoid であり、Universal mapping property で結びついています。 これ
は後で詳しく見ます。
最後は Sets 集合の圏です。射は、Set 間の写像です。圏の性質のほとんどは自明 (refl ) です。_o_ = _o_ のような同じようで違う記号が出てくるのが Agda らしいところです。
Sets では、対象をAgdaの集合、Agda の関数そのものを射としています。対象の集合のレベルは決まっています。
module Category.Sets where
open import Category
open import Relation.Binary.Core
open import Relation.Binary
open import Level
_o_ : ∀{ℓ} {A B C : Set ℓ} → (f : B → C) → (g : A → B) → A → C
_o_ f g x = f (g x)
_-Set⟶_ : ∀{ℓ} → (A B : Set ℓ) → Set _
A -Set⟶ B = A → B
SetId : ∀{ℓ} {A : Set ℓ} → A → A
SetId x = x
Sets : ∀{ℓ} → Category _ _ ℓ
Sets {ℓ} = record { Obj = Set ℓ
; Hom = _-Set⟶_
; _o_ = _o_
; _≈_ = _≡_
; isCategory = isCategory
}
where
isCategory : IsCategory (Set ℓ) _-Set⟶_ _≡_ _o_ SetId
isCategory = record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}
; identityL = refl
; identityR = refl
; o-resp-≈ = o-resp-≈
; associative = refl
}
where
o-resp-≈ : {A B C : Set ℓ} {f g : A -Set⟶ B} {h i : B -Set⟶ C}
→ f ≡ g → h ≡ i → h o f ≡ i o g
o-resp-≈ refl refl = refl
Sets はある Level の Set に対して定義されています。この三つの圏の特徴は、_≈_ = _≡_ であることです。このために、cong : x ≡ y -> f x ≡ f y を使うことができます。
このSets は、Monoid と組み合わせて Monad の例 で使います。