|
0
|
1
|
|
|
2
|
|
|
3 module nat where
|
|
|
4
|
|
|
5
|
|
|
6 -- Monad
|
|
|
7 -- Category A
|
|
|
8
|
|
|
9 -- A = Category
|
|
|
10
|
|
|
11 -- Functor T : A -> A
|
|
|
12
|
|
|
13
|
|
|
14
|
|
|
15 --T(a) = t(a)
|
|
|
16 --T(f) = tf(f)
|
|
|
17
|
|
|
18 --T(g f) = T(g) T(f)
|
|
|
19
|
|
|
20 open import Category
|
|
|
21 open import Level
|
|
|
22 open Functor
|
|
|
23
|
|
|
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 }
|
|
|
25 -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
|
|
|
26 Lemma1 = \t -> IsFunctor.distr ( isFunctor t )
|
|
|
27
|
|
|
28
|
|
|
29
|
|
|
30
|
|
|
31 -- F(f)
|
|
|
32 -- F(a) ----> F(b)
|
|
|
33 -- | |
|
|
|
34 -- |t(a) |t(b) G(f)t(a) = t(b)F(f)
|
|
|
35 -- | |
|
|
|
36 -- v v
|
|
|
37 -- G(a) ----> G(b)
|
|
|
38 -- G(f)
|
|
|
39
|
|
|
40 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
|
|
|
41 ( F G : Functor D C )
|
|
|
42 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
|
|
|
43 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
|
44 field
|
|
|
45 naturality : {a b : Obj D} {f : Hom D a b}
|
|
|
46 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ]
|
|
|
47 -- how to write uniquness?
|
|
|
48 -- uniqness : {d : Obj D}
|
|
|
49 -- → ∃{e : Trans d} -> ∀{a : Trans d} → C [ e ≈ a ]
|
|
|
50
|
|
|
51
|
|
|
52 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
|
|
|
53 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
|
54 field
|
|
|
55 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
|
|
|
56 isNTrans : IsNTrans domain codomain F G Trans
|
|
|
57
|
|
|
58 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 }
|
|
|
60 -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ]
|
|
|
61 Lemma2 = \n -> IsNTrans.naturality ( isNTrans n )
|
|
|
62
|
|
|
63 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
|
|
|
74 -- η : 1_A -> T
|
|
|
75 -- μ : TT -> T
|
|
|
76 -- μ(a)η(T(a)) = a
|
|
|
77 -- μ(a)T(η(a)) = a
|
|
|
78 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
|
|
|
79
|
|
|
80
|
|
|
81
|
|
|
82
|
|
|
83
|
|
|
84 -- nat of η
|
|
|
85
|
|
|
86
|
|
|
87 -- g ○ f = μ(c) T(g) f
|
|
|
88
|
|
|
89 -- h ○ (g ○ f) = (h ○ g) ○ f
|
|
|
90
|
|
|
91 -- η(b) ○ f = f
|
|
|
92 -- f ○ η(a) = f
|
|
|
93
|
|
|
94
|
