|
56
|
1 module cat-utility where
|
|
|
2
|
|
|
3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
|
4
|
|
87
|
5 open import Category -- https://github.com/konn/category-agda
|
|
|
6 open import Level
|
|
|
7 --open import Category.HomReasoning
|
|
|
8 open import HomReasoning
|
|
56
|
9
|
|
87
|
10 open Functor
|
|
56
|
11
|
|
87
|
12 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a
|
|
|
13 id1 A a = (Id {_} {_} {_} {A} a)
|
|
56
|
14
|
|
87
|
15 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
16 ( U : Functor B A )
|
|
|
17 ( F : Obj A → Obj B )
|
|
|
18 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
|
|
|
19 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b )
|
|
|
20 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
21 field
|
|
|
22 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
|
|
|
23 A [ A [ FMap U ( f * ) o η a' ] ≈ f ]
|
|
|
24 uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } →
|
|
|
25 A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ]
|
|
56
|
26
|
|
87
|
27 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
28 ( U : Functor B A )
|
|
|
29 ( F : Obj A → Obj B )
|
|
|
30 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
|
|
|
31 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
32 infixr 11 _*
|
|
|
33 field
|
|
|
34 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
|
|
|
35 isUniversalMapping : IsUniversalMapping A B U F η _*
|
|
56
|
36
|
|
87
|
37 open NTrans
|
|
|
38 open import Category.Cat
|
|
|
39 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
40 ( U : Functor B A )
|
|
|
41 ( F : Functor A B )
|
|
|
42 ( η : NTrans A A identityFunctor ( U ○ F ) )
|
|
|
43 ( ε : NTrans B B ( F ○ U ) identityFunctor )
|
|
|
44 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
45 field
|
|
|
46 adjoint1 : { b : Obj B } →
|
|
|
47 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
|
|
|
48 adjoint2 : {a : Obj A} →
|
|
|
49 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
|
|
56
|
50
|
|
87
|
51 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
52 ( U : Functor B A )
|
|
|
53 ( F : Functor A B )
|
|
|
54 ( η : NTrans A A identityFunctor ( U ○ F ) )
|
|
|
55 ( ε : NTrans B B ( F ○ U ) identityFunctor )
|
|
|
56 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
57 field
|
|
|
58 isAdjunction : IsAdjunction A B U F η ε
|
|
56
|
59
|
|
|
60
|
|
87
|
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 [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
|
|
|
68 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
|
69 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
56
|
70
|
|
87
|
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 eta : NTrans A A identityFunctor T
|
|
|
74 eta = η
|
|
|
75 mu : NTrans A A (T ○ T) T
|
|
|
76 mu = μ
|
|
|
77 field
|
|
|
78 isMonad : IsMonad A T η μ
|
|
56
|
79
|
|
87
|
80 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
|
|
|
81 (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H)
|
|
|
82 Functor*Nat A {B} C F {G} {H} n = record {
|
|
|
83 TMap = \a -> FMap F (TMap n a)
|
|
|
84 ; isNTrans = record {
|
|
|
85 naturality = naturality
|
|
|
86 }
|
|
|
87 } where
|
|
|
88 naturality : {a b : Obj A} {f : Hom A a b}
|
|
|
89 → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ]
|
|
|
90 naturality {a} {b} {f} = let open ≈-Reasoning (C) in
|
|
|
91 begin
|
|
|
92 (FMap F ( FMap H f )) o ( FMap F (TMap n a))
|
|
|
93 ≈⟨ sym (distr F) ⟩
|
|
|
94 FMap F ( B [ (FMap H f) o TMap n a ])
|
|
|
95 ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
|
|
|
96 FMap F ( B [ (TMap n b ) o FMap G f ] )
|
|
|
97 ≈⟨ distr F ⟩
|
|
|
98 (FMap F (TMap n b )) o (FMap F (FMap G f))
|
|
|
99 ∎
|
|
56
|
100
|
|
87
|
101 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
|
|
|
102 { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F)
|
|
|
103 Nat*Functor A {B} C {G} {H} n F = record {
|
|
|
104 TMap = \a -> TMap n (FObj F a)
|
|
|
105 ; isNTrans = record {
|
|
|
106 naturality = naturality
|
|
|
107 }
|
|
|
108 } where
|
|
|
109 naturality : {a b : Obj A} {f : Hom A a b}
|
|
|
110 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ]
|
|
|
111 naturality {a} {b} {f} = IsNTrans.naturality ( isNTrans n)
|
|
56
|
112
|
|
87
|
113 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
|
|
|
114 ( T : Functor A A )
|
|
|
115 ( η : NTrans A A identityFunctor T )
|
|
|
116 ( μ : NTrans A A (T ○ T) T )
|
|
|
117 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
|
118 monad : Monad A T η μ
|
|
|
119 monad = M
|
|
|
120 -- g ○ f = μ(c) T(g) f
|
|
|
121 join : { a b : Obj A } → { c : Obj A } →
|
|
|
122 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c )
|
|
|
123 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ]
|
|
56
|
124
|
|
87
|
125 -- T ≃ (U_R ○ F_R)
|
|
|
126 -- μ = U_R ε F_R
|
|
|
127 -- nat-ε
|
|
|
128 -- nat-η -- same as η but has different types
|
|
84
|
129
|
|
87
|
130 record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' )
|
|
|
131 ( T : Functor A A )
|
|
|
132 { η : NTrans A A identityFunctor T }
|
|
|
133 { μ : NTrans A A (T ○ T) T }
|
|
|
134 ( M : Monad A T η μ )
|
|
|
135 ( UR : Functor B A ) ( FR : Functor A B )
|
|
|
136 { ηR : NTrans A A identityFunctor ( UR ○ FR ) }
|
|
|
137 { εR : NTrans B B ( FR ○ UR ) identityFunctor }
|
|
|
138 { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) }
|
|
|
139 ( Adj : Adjunction A B UR FR ηR εR )
|
|
|
140 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
141 field
|
|
|
142 T=UF : T ≃ (UR ○ FR)
|
|
|
143 μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
|
|
|
144 -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ]
|
|
|
145 -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ]
|
|
86
|
146
|
