Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 103:8dcf926482af
on oging
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Jul 2013 15:42:38 +0900 |
| parents | 51f653bd9656 |
| children | 5f331dfc000b |
| rev | line source |
|---|---|
| 31 | 1 module universal-mapping where |
| 2 | |
| 56 | 3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
| 4 | |
| 31 | 5 open import Category -- https://github.com/konn/category-agda |
| 6 open import Level | |
| 56 | 7 open import HomReasoning |
| 31 | 8 |
| 9 open Functor | |
| 37 | 10 |
| 46 | 11 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
| 12 id1 A a = (Id {_} {_} {_} {A} a) | |
| 13 | |
| 31 | 14 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 15 ( U : Functor B A ) | |
| 56 | 16 ( F : Obj A → Obj B ) |
| 17 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 18 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) | |
| 31 | 19 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where |
| 20 field | |
| 56 | 21 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → |
| 37 | 22 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
| 56 | 23 uniquness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (F a') b' } → |
| 24 A [ A [ FMap U g o η a' ] ≈ f ] → B [ f * ≈ g ] | |
| 31 | 25 |
| 26 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 27 ( U : Functor B A ) | |
| 56 | 28 ( F : Obj A → Obj B ) |
| 29 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) | |
| 31 | 30 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where |
| 37 | 31 infixr 11 _* |
| 31 | 32 field |
| 56 | 33 _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b |
| 31 | 34 isUniversalMapping : IsUniversalMapping A B U F η _* |
| 35 | |
| 32 | 36 open NTrans |
| 37 open import Category.Cat | |
| 38 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 39 ( U : Functor B A ) | |
| 40 ( F : Functor A B ) | |
| 41 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 42 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 43 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 44 field | |
| 56 | 45 adjoint1 : { b' : Obj B } → |
| 46 | 46 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ id1 A (FObj U b') ] |
| 56 | 47 adjoint2 : {a' : Obj A} → |
| 46 | 48 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ id1 B (FObj F a') ] |
| 31 | 49 |
| 32 | 50 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 51 ( U : Functor B A ) | |
| 52 ( F : Functor A B ) | |
| 53 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 54 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 55 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 56 field | |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
57 isAdjunction : IsAdjunction A B U F η ε |
| 32 | 58 |
| 43 | 59 -- |
| 60 -- Adjunction yields solution of universal mapping | |
| 61 -- | |
| 62 -- | |
| 63 | |
| 34 | 64 open Adjunction |
| 65 open UniversalMapping | |
| 35 | 66 |
| 56 | 67 Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 54 | 68 { U : Functor B A } |
| 69 { F : Functor A B } | |
| 70 { η : NTrans A A identityFunctor ( U ○ F ) } | |
| 56 | 71 { ε : NTrans B B ( F ○ U ) identityFunctor } → |
| 72 Adjunction A B U F η ε → UniversalMapping A B U (FObj F) (TMap η) | |
| 73 Adj2UM A B {U} {F} {η} {ε} adj = record { | |
| 43 | 74 _* = solution ; |
| 36 | 75 isUniversalMapping = record { |
| 43 | 76 universalMapping = universalMapping; |
| 51 | 77 uniquness = uniqness |
| 36 | 78 } |
| 79 } where | |
| 56 | 80 solution : { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) → Hom B (FObj F a ) b |
| 43 | 81 solution {_} {b} f = B [ TMap ε b o FMap F f ] |
| 56 | 82 universalMapping : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → |
| 43 | 83 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] |
| 51 | 84 universalMapping {a} {b} {f} = |
| 38 | 85 let open ≈-Reasoning (A) in |
| 86 begin | |
| 43 | 87 FMap U ( solution f) o TMap η a |
| 39 | 88 ≈⟨⟩ |
| 89 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a | |
| 66 | 90 ≈⟨ car (distr U ) ⟩ |
| 39 | 91 ( (FMap U (TMap ε b)) o (FMap U ( FMap F f )) ) o TMap η a |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
92 ≈⟨ sym assoc ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
93 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a ) |
| 66 | 94 ≈⟨ cdr (nat η) ⟩ |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
95 (FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f ) |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
96 ≈⟨ assoc ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
97 ((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
98 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
99 id (FObj U b) o f |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
100 ≈⟨ idL ⟩ |
| 38 | 101 f |
| 102 ∎ | |
| 56 | 103 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g : Hom B (FObj F a) b) → |
| 104 A [ A [ FMap U g o TMap η a ] ≈ f ] → | |
| 44 | 105 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] |
| 106 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k | |
| 56 | 107 uniqness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} → |
| 108 A [ A [ FMap U g o TMap η a' ] ≈ f ] → B [ solution f ≈ g ] | |
| 52 | 109 uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in |
| 44 | 110 begin |
| 111 solution f | |
| 112 ≈⟨⟩ | |
| 113 TMap ε b o FMap F f | |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
114 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ |
| 44 | 115 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] ) |
| 66 | 116 ≈⟨ cdr (distr F ) ⟩ |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
117 TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) ) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
118 ≈⟨ assoc ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
119 ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a ) |
| 66 | 120 ≈⟨ sym ( car ( nat ε )) ⟩ |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
121 ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a ) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
122 ≈⟨ sym assoc ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
123 g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) ) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
124 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
125 g o id (FObj F a) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
126 ≈⟨ idR ⟩ |
| 44 | 127 g |
| 128 ∎ | |
| 129 | |
| 43 | 130 -- |
| 131 -- | |
| 132 -- Universal mapping yields Adjunction | |
| 133 -- | |
| 134 -- | |
| 135 | |
| 136 | |
| 137 -- | |
| 138 -- F is an functor | |
| 139 -- | |
| 140 | |
| 54 | 141 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 142 { U : Functor B A } | |
| 56 | 143 { F : Obj A → Obj B } |
| 144 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 145 UniversalMapping A B U F η → Functor A B | |
| 54 | 146 FunctorF A B {U} {F} {η} um = record { |
| 41 | 147 FObj = F; |
| 42 | 148 FMap = myFMap ; |
| 149 isFunctor = myIsFunctor | |
| 41 | 150 } where |
| 56 | 151 myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b) |
| 42 | 152 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) |
| 56 | 153 lemma-id1 : {a : Obj A} → A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ] |
| 46 | 154 lemma-id1 {a} = let open ≈-Reasoning (A) in |
| 42 | 155 begin |
| 46 | 156 FMap U (id1 B (F a)) o η a |
| 42 | 157 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩ |
| 46 | 158 id (FObj U ( F a )) o η a |
| 42 | 159 ≈⟨ idL ⟩ |
| 160 η a | |
| 161 ≈⟨ sym idR ⟩ | |
| 46 | 162 η a o id a |
| 42 | 163 ∎ |
| 46 | 164 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] |
| 52 | 165 lemma-id {a} = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) lemma-id1 |
| 46 | 166 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → |
| 167 A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] | |
| 168 lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in | |
| 169 begin | |
| 170 ( FMap U ((_* um) (A [ η b o g ]) )) o η a | |
| 51 | 171 ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 46 | 172 η b o g |
| 173 ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ | |
| 174 η b o f | |
| 175 ∎ | |
| 176 lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b o f ] ) ≈ (_* um) (A [ η b o g ]) ] | |
| 52 | 177 lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) ( lemma-cong2 a b f g eq ) |
| 46 | 178 lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] |
| 179 lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq | |
| 47 | 180 lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → |
| 181 A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ]) o η a ] ≈ (A [ η c o A [ g o f ] ]) ] | |
| 182 lemma-distr2 a b c f g = let open ≈-Reasoning (A) in | |
| 183 begin | |
| 184 ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a | |
| 66 | 185 ≈⟨ car (distr U ) ⟩ |
| 47 | 186 (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a |
| 187 ≈⟨ sym assoc ⟩ | |
| 188 ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) | |
| 51 | 189 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 190 ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) |
| 191 ≈⟨ assoc ⟩ | |
| 192 ( FMap U ((_* um) (A [ η c o g ])) o η b) o f | |
| 51 | 193 ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 194 ( η c o g ) o f |
| 195 ≈⟨ sym assoc ⟩ | |
| 196 η c o ( g o f ) | |
| 197 ∎ | |
| 198 lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → | |
| 199 B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] | |
| 52 | 200 lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( isUniversalMapping um )) (lemma-distr2 a b c f g ) |
| 47 | 201 lemma-distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )] |
| 202 lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g | |
| 42 | 203 myIsFunctor : IsFunctor A B F myFMap |
| 204 myIsFunctor = | |
| 46 | 205 record { ≈-cong = lemma-cong |
| 42 | 206 ; identity = lemma-id |
| 47 | 207 ; distr = lemma-distr |
| 42 | 208 } |
| 41 | 209 |
| 48 | 210 -- |
| 211 -- naturality of η | |
| 212 -- | |
| 213 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 54 | 214 { U : Functor B A } |
| 56 | 215 { F : Obj A → Obj B } |
| 216 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 217 (um : UniversalMapping A B U F η ) → | |
| 54 | 218 NTrans A A identityFunctor ( U ○ FunctorF A B um ) |
| 219 nat-η A B {U} {F} {η} um = record { | |
| 48 | 220 TMap = η ; isNTrans = myIsNTrans |
| 221 } where | |
| 222 F' : Functor A B | |
| 54 | 223 F' = FunctorF A B um |
| 48 | 224 naturality : {a b : Obj A} {f : Hom A a b} |
| 225 → A [ A [ (FMap U (FMap F' f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] | |
| 49 | 226 naturality {a} {b} {f} = let open ≈-Reasoning (A) in |
| 227 begin | |
| 228 (FMap U (FMap F' f)) o ( η a ) | |
| 229 ≈⟨⟩ | |
| 230 (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) | |
| 51 | 231 ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 49 | 232 (η b ) o f |
| 233 ∎ | |
| 48 | 234 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η |
| 235 myIsNTrans = record { naturality = naturality } | |
| 49 | 236 |
| 237 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 54 | 238 { U : Functor B A } |
| 56 | 239 { F : Obj A → Obj B } |
| 240 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } → | |
| 241 (um : UniversalMapping A B U F η ) → | |
| 54 | 242 NTrans B B ( FunctorF A B um ○ U) identityFunctor |
| 243 nat-ε A B {U} {F} {η} um = record { | |
| 49 | 244 TMap = ε ; isNTrans = myIsNTrans |
| 245 } where | |
| 246 F' : Functor A B | |
| 54 | 247 F' = FunctorF A B um |
| 56 | 248 ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b |
| 49 | 249 ε b = (_* um) ( id1 A (FObj U b)) |
| 56 | 250 lemma-nat1 : (a b : Obj B) (f : Hom B a b ) → |
| 51 | 251 A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] ) o η (FObj U a) ] |
| 252 ≈ A [ FMap U f o id1 A (FObj U a) ] ] | |
| 253 lemma-nat1 a b f = let open ≈-Reasoning (A) in | |
| 254 begin | |
| 255 FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] ) o η (FObj U a) | |
| 66 | 256 ≈⟨ car ( distr U ) ⟩ |
| 51 | 257 ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a) |
| 258 ≈⟨ sym assoc ⟩ | |
| 259 FMap U ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f ))) o η (FObj U a) | |
| 260 ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 261 FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f ) | |
| 262 ≈⟨ assoc ⟩ | |
| 263 (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f | |
| 264 ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 265 id1 A (FObj U b) o FMap U f | |
| 266 ≈⟨ idL ⟩ | |
| 267 FMap U f | |
| 268 ≈⟨ sym idR ⟩ | |
| 269 FMap U f o id (FObj U a) | |
| 270 ∎ | |
| 56 | 271 lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ] |
| 52 | 272 ≈ A [ FMap U f o id1 A (FObj U a) ] ] |
| 273 lemma-nat2 a b f = let open ≈-Reasoning (A) in | |
| 274 begin | |
| 275 FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ]) o η (FObj U a) | |
| 66 | 276 ≈⟨ car ( distr U ) ⟩ |
| 52 | 277 (FMap U f o FMap U ((um *) (id1 A (FObj U a )))) o η (FObj U a) |
| 278 ≈⟨ sym assoc ⟩ | |
| 279 FMap U f o ( FMap U ((um *) (id1 A (FObj U a ))) o η (FObj U a) ) | |
| 280 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ | |
| 281 FMap U f o id (FObj U a ) | |
| 282 ∎ | |
| 49 | 283 naturality : {a b : Obj B} {f : Hom B a b } |
| 284 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ] | |
| 285 naturality {a} {b} {f} = let open ≈-Reasoning (B) in | |
| 286 sym ( begin | |
| 287 ε b o (FMap F' (FMap U f)) | |
| 288 ≈⟨⟩ | |
| 50 | 289 ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) |
| 290 ≈⟨⟩ | |
| 291 ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) | |
| 52 | 292 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat1 a b f))) ⟩ |
| 51 | 293 (_* um) ( A [ FMap U f o id1 A (FObj U a) ] ) |
| 52 | 294 ≈⟨ (IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-nat2 a b f)) ⟩ |
| 50 | 295 f o ((_* um) ( id1 A (FObj U a))) |
| 296 ≈⟨⟩ | |
| 49 | 297 f o (ε a) |
| 298 ∎ ) | |
| 299 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε | |
| 300 myIsNTrans = record { naturality = naturality } | |
| 53 | 301 |
| 302 ------ | |
| 303 -- | |
| 304 -- Adjunction Construction from Universal Mapping | |
| 305 -- | |
| 306 ----- | |
| 307 | |
| 308 UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 309 ( U : Functor B A ) | |
| 56 | 310 ( F' : Obj A → Obj B ) |
| 311 ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) → | |
| 312 (um : UniversalMapping A B U F' η' ) → | |
| 54 | 313 Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B um) |
| 53 | 314 UMAdjunction A B U F' η' um = record { |
| 315 isAdjunction = record { | |
| 316 adjoint1 = adjoint1 ; | |
| 317 adjoint2 = adjoint2 | |
| 318 } | |
| 319 } where | |
| 320 F : Functor A B | |
| 54 | 321 F = FunctorF A B um |
| 53 | 322 η : NTrans A A identityFunctor ( U ○ F ) |
| 54 | 323 η = nat-η A B um |
| 53 | 324 ε : NTrans B B ( F ○ U ) identityFunctor |
| 54 | 325 ε = nat-ε A B um |
| 56 | 326 adjoint1 : { b : Obj B } → |
| 53 | 327 A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
328 adjoint1 {b} = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
329 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
330 FMap U ( TMap ε b ) o TMap η ( FObj U b ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
331 ≈⟨⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
332 FMap U ((_* um) ( id1 A (FObj U b))) o η' ( FObj U b ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
333 ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um ) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
334 id (FObj U b) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
335 ∎ |
| 56 | 336 lemma-adj1 : (a : Obj A) → |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
337 A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ] |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
338 ≈ (η' a) ] |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
339 lemma-adj1 a = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
340 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
341 FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a |
| 66 | 342 ≈⟨ car (distr U) ⟩ |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
343 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
344 ≈⟨ sym assoc ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
345 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
346 ≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
347 FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
348 ≈⟨ assoc ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
349 (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
350 ≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
351 id (FObj U ( FObj F a)) o ( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
352 ≈⟨ idL ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
353 η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
354 ∎ |
| 56 | 355 lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈ η' a ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
356 lemma-adj2 a = let open ≈-Reasoning (A) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
357 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
358 FMap U (id1 B (FObj F a)) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
359 ≈⟨ car ( IsFunctor.identity ( isFunctor U)) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
360 id (FObj U (FObj F a)) o η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
361 ≈⟨ idL ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
362 η' a |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
363 ∎ |
| 56 | 364 adjoint2 : {a : Obj A} → |
| 53 | 365 B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] |
|
55
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
366 adjoint2 {a} = let open ≈-Reasoning (B) in |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
367 begin |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
368 TMap ε ( FObj F a ) o FMap F ( TMap η a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
369 ≈⟨⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
370 ((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
371 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj1 a))) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
372 (_* um)( η' a ) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
373 ≈⟨ IsUniversalMapping.uniquness ( isUniversalMapping um ) (lemma-adj2 a) ⟩ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
374 id1 B (FObj F a) |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
375 ∎ |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
376 |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
377 |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
378 -- done! |
|
1716403c92c2
Adjoint proved. All done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
54
diff
changeset
|
379 |