Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 1:73b780d13f60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Jul 2013 02:15:24 +0900
parents 302941542c0f
children 7ce421d5ee2b
comparison
equal deleted inserted replaced
0:302941542c0f 1:73b780d13f60
1
2
3 module nat where 1 module nat where
4
5 2
6 -- Monad 3 -- Monad
7 -- Category A 4 -- Category A
8
9 -- A = Category 5 -- A = Category
10
11 -- Functor T : A -> A 6 -- Functor T : A -> A
12
13
14
15 --T(a) = t(a) 7 --T(a) = t(a)
16 --T(f) = tf(f) 8 --T(f) = tf(f)
17
18 --T(g f) = T(g) T(f)
19 9
20 open import Category 10 open import Category
21 open import Level 11 open import Level
22 open Functor 12 open Functor
23 13
14 --T(g f) = T(g) T(f)
15
24 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 } 16 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 }
25 -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] 17 -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
26 Lemma1 = \t -> IsFunctor.distr ( isFunctor t ) 18 Lemma1 = \t -> IsFunctor.distr ( isFunctor t )
27
28
29
30 19
31 -- F(f) 20 -- F(f)
32 -- F(a) ----> F(b) 21 -- F(a) ----> F(b)
33 -- | | 22 -- | |
34 -- |t(a) |t(b) G(f)t(a) = t(b)F(f) 23 -- |t(a) |t(b) G(f)t(a) = t(b)F(f)
54 field 43 field
55 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) 44 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
56 isNTrans : IsNTrans domain codomain F G Trans 45 isNTrans : IsNTrans domain codomain F G Trans
57 46
58 open NTrans 47 open NTrans
59 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b } 48 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A}
60 -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] 49 -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b }
50 -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ]
61 Lemma2 = \n -> IsNTrans.naturality ( isNTrans n ) 51 Lemma2 = \n -> IsNTrans.naturality ( isNTrans n )
62 52
63 open import Category.Cat 53 open import Category.Cat
64
65 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
66 ( T : Functor A A )
67 ( η : NTrans A A (identityFunctor) T )
68 ( μ : NTrans A A T (T ○ T))
69 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
70 field
71 unity1 : {a b : Obj A}
72 → A [ A [ ( Trans μ a ) o ( Trans η a) ] ≈ Id A a ]
73 54
74 -- η : 1_A -> T 55 -- η : 1_A -> T
75 -- μ : TT -> T 56 -- μ : TT -> T
76 -- μ(a)η(T(a)) = a 57 -- μ(a)η(T(a)) = a
77 -- μ(a)T(η(a)) = a 58 -- μ(a)T(η(a)) = a
78 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) 59 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
79 60
61 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
62 ( T : Functor A A )
63 ( η : NTrans A A identityFunctor T )
64 ( μ : NTrans A A (T ○ T) T)
65 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
66 field
67 assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ]
68 -- unity2 : {a : Obj A} -> A [ Trans μ a o (FMap T (Trans η a )) ]
69 -- unity1 : {a : Obj A} -> A [ Trans μ a o Trans η ( FObj T a ) ]
80 70
81 71 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
72 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
73 field
74 isMonad : IsMonad A T η μ
82 75
83 76
84 -- nat of η 77 -- nat of η
85 78
86 79