Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 51:adc6bd3c9270
on going...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 16:01:25 +0900 |
| parents | b518af3a9b07 |
| children | 0fc0dbda7b55 |
| rev | line source |
|---|---|
| 31 | 1 module universal-mapping where |
| 2 | |
| 3 open import Category -- https://github.com/konn/category-agda | |
| 4 open import Level | |
| 5 open import Category.HomReasoning | |
| 6 | |
| 7 open Functor | |
| 37 | 8 |
| 46 | 9 id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a |
| 10 id1 A a = (Id {_} {_} {_} {A} a) | |
| 11 | |
| 31 | 12 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 13 ( U : Functor B A ) | |
| 14 ( F : Obj A -> Obj B ) | |
| 15 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 16 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
| 17 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 18 field | |
| 51 | 19 universalMapping : {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> |
| 37 | 20 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
| 51 | 21 uniquness : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g : Hom B (F a') b' } -> |
| 42 | 22 A [ A [ FMap U g o η a' ] ≈ f ] -> B [ f * ≈ g ] |
| 31 | 23 |
| 24 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 25 ( U : Functor B A ) | |
| 26 ( F : Obj A -> Obj B ) | |
| 27 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 28 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 37 | 29 infixr 11 _* |
| 31 | 30 field |
| 37 | 31 _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b |
| 31 | 32 isUniversalMapping : IsUniversalMapping A B U F η _* |
| 33 | |
| 32 | 34 open NTrans |
| 35 open import Category.Cat | |
| 36 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 37 ( U : Functor B A ) | |
| 38 ( F : Functor A B ) | |
| 39 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 40 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 42 field | |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
43 adjoint1 : { b' : Obj B } -> |
| 46 | 44 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ id1 A (FObj U b') ] |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
45 adjoint2 : {a' : Obj A} -> |
| 46 | 46 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ id1 B (FObj F a') ] |
| 31 | 47 |
| 32 | 48 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 49 ( U : Functor B A ) | |
| 50 ( F : Functor A B ) | |
| 51 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 52 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 53 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 54 field | |
|
40
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
55 isAdjunction : IsAdjunction A B U F η ε |
| 32 | 56 |
| 43 | 57 -- |
| 58 -- Adjunction yields solution of universal mapping | |
| 59 -- | |
| 60 -- | |
| 61 | |
| 34 | 62 open Adjunction |
| 63 open UniversalMapping | |
| 35 | 64 |
|
33
fefebc387eae
add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
65 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 35 | 66 ( U : Functor B A ) |
| 67 ( F : Functor A B ) | |
| 68 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 69 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
| 37 | 70 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) |
| 35 | 71 Lemma1 A B U F η ε adj = record { |
| 43 | 72 _* = solution ; |
| 36 | 73 isUniversalMapping = record { |
| 43 | 74 universalMapping = universalMapping; |
| 51 | 75 uniquness = uniqness |
| 36 | 76 } |
| 77 } where | |
| 43 | 78 solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b |
| 79 solution {_} {b} f = B [ TMap ε b o FMap F f ] | |
| 51 | 80 universalMapping : {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> |
| 43 | 81 A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] |
| 51 | 82 universalMapping {a} {b} {f} = |
| 38 | 83 let open ≈-Reasoning (A) in |
| 84 begin | |
| 43 | 85 FMap U ( solution f) o TMap η a |
| 39 | 86 ≈⟨⟩ |
| 87 FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a | |
| 88 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ | |
| 89 ( (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
|
90 ≈⟨ sym assoc ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
91 (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a ) |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
92 ≈⟨ cdr (nat A η) ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
93 (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
|
94 ≈⟨ assoc ⟩ |
|
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 ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
97 id (FObj U b) o f |
|
c34b1cfe9fdc
Adjunction to Universal Mapping end
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
98 ≈⟨ idL ⟩ |
| 38 | 99 f |
| 100 ∎ | |
| 44 | 101 lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g : Hom B (FObj F a) b) -> |
| 102 A [ A [ FMap U g o TMap η a ] ≈ f ] -> | |
| 103 B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] | |
| 104 lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k | |
| 51 | 105 uniqness : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g : Hom B (FObj F a') b'} -> |
| 43 | 106 A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] |
| 51 | 107 uniqness a b {f} {g} k = let open ≈-Reasoning (B) in |
| 44 | 108 begin |
| 109 solution f | |
| 110 ≈⟨⟩ | |
| 111 TMap ε b o FMap F f | |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
112 ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ |
| 44 | 113 TMap ε b o FMap F ( A [ FMap U g o TMap η a ] ) |
|
45
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
114 ≈⟨ cdr (IsFunctor.distr ( isFunctor F )) ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
115 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
|
116 ≈⟨ assoc ⟩ |
|
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 ≈⟨ sym ( car ( nat B ε )) ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
119 ( 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
|
120 ≈⟨ sym assoc ⟩ |
|
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 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
123 g o id (FObj F a) |
|
659b8a21caf7
uniq-univeralMapping from Adjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
124 ≈⟨ idR ⟩ |
| 44 | 125 g |
| 126 ∎ | |
| 127 | |
| 43 | 128 -- |
| 129 -- | |
| 130 -- Universal mapping yields Adjunction | |
| 131 -- | |
| 132 -- | |
| 133 | |
| 134 | |
| 135 -- | |
| 136 -- F is an functor | |
| 137 -- | |
| 138 | |
| 41 | 139 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 140 ( U : Functor B A ) | |
| 141 ( F : Obj A -> Obj B ) | |
| 142 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
| 143 UniversalMapping A B U F η -> Functor A B | |
| 144 FunctorF A B U F η um = record { | |
| 145 FObj = F; | |
| 42 | 146 FMap = myFMap ; |
| 147 isFunctor = myIsFunctor | |
| 41 | 148 } where |
| 42 | 149 myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b) |
| 150 myFMap f = (_* um) (A [ η (Category.cod A f ) o f ]) | |
| 46 | 151 lemma-id1 : {a : Obj A} -> A [ A [ FMap U (id1 B (F a)) o η a ] ≈ (A [ (η a) o (id1 A a) ]) ] |
| 152 lemma-id1 {a} = let open ≈-Reasoning (A) in | |
| 42 | 153 begin |
| 46 | 154 FMap U (id1 B (F a)) o η a |
| 42 | 155 ≈⟨ ( car ( IsFunctor.identity ( isFunctor U ))) ⟩ |
| 46 | 156 id (FObj U ( F a )) o η a |
| 42 | 157 ≈⟨ idL ⟩ |
| 158 η a | |
| 159 ≈⟨ sym idR ⟩ | |
| 46 | 160 η a o id a |
| 42 | 161 ∎ |
| 46 | 162 lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] |
| 51 | 163 lemma-id {a} = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F a) lemma-id1 |
| 46 | 164 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → |
| 165 A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] | |
| 166 lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in | |
| 167 begin | |
| 168 ( FMap U ((_* um) (A [ η b o g ]) )) o η a | |
| 51 | 169 ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 46 | 170 η b o g |
| 171 ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ | |
| 172 η b o f | |
| 173 ∎ | |
| 174 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 ]) ] | |
| 51 | 175 lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F b) ( lemma-cong2 a b f g eq ) |
| 46 | 176 lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] |
| 177 lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq | |
| 47 | 178 lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → |
| 179 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 ] ]) ] | |
| 180 lemma-distr2 a b c f g = let open ≈-Reasoning (A) in | |
| 181 begin | |
| 182 ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a | |
| 183 ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ | |
| 184 (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a | |
| 185 ≈⟨ sym assoc ⟩ | |
| 186 ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) | |
| 51 | 187 ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 188 ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) |
| 189 ≈⟨ assoc ⟩ | |
| 190 ( FMap U ((_* um) (A [ η c o g ])) o η b) o f | |
| 51 | 191 ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 47 | 192 ( η c o g ) o f |
| 193 ≈⟨ sym assoc ⟩ | |
| 194 η c o ( g o f ) | |
| 195 ∎ | |
| 196 lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → | |
| 197 B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] | |
| 51 | 198 lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) a (F c)) (lemma-distr2 a b c f g ) |
| 47 | 199 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 ] )] |
| 200 lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g | |
| 42 | 201 myIsFunctor : IsFunctor A B F myFMap |
| 202 myIsFunctor = | |
| 46 | 203 record { ≈-cong = lemma-cong |
| 42 | 204 ; identity = lemma-id |
| 47 | 205 ; distr = lemma-distr |
| 42 | 206 } |
| 41 | 207 |
| 48 | 208 -- |
| 209 -- naturality of η | |
| 210 -- | |
| 211 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 212 ( U : Functor B A ) | |
| 213 ( F : Obj A -> Obj B ) | |
| 214 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
| 215 (um : UniversalMapping A B U F η ) -> | |
| 49 | 216 NTrans A A identityFunctor ( U ○ FunctorF A B U F η um ) |
| 48 | 217 nat-η A B U F η um = record { |
| 218 TMap = η ; isNTrans = myIsNTrans | |
| 219 } where | |
| 220 F' : Functor A B | |
| 221 F' = FunctorF A B U F η um | |
| 222 naturality : {a b : Obj A} {f : Hom A a b} | |
| 223 → A [ A [ (FMap U (FMap F' f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] | |
| 49 | 224 naturality {a} {b} {f} = let open ≈-Reasoning (A) in |
| 225 begin | |
| 226 (FMap U (FMap F' f)) o ( η a ) | |
| 227 ≈⟨⟩ | |
| 228 (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) | |
| 51 | 229 ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ |
| 49 | 230 (η b ) o f |
| 231 ∎ | |
| 48 | 232 myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η |
| 233 myIsNTrans = record { naturality = naturality } | |
| 49 | 234 |
| 235 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 236 ( U : Functor B A ) | |
| 237 ( F : Obj A -> Obj B ) | |
| 238 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) -> | |
| 239 (um : UniversalMapping A B U F η ) -> | |
| 240 NTrans B B ( FunctorF A B U F η um ○ U) identityFunctor | |
| 241 nat-ε A B U F η um = record { | |
| 242 TMap = ε ; isNTrans = myIsNTrans | |
| 243 } where | |
| 244 F' : Functor A B | |
| 245 F' = FunctorF A B U F η um | |
| 246 ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b | |
| 247 ε b = (_* um) ( id1 A (FObj U b)) | |
| 51 | 248 lemma-nat1 : (a b : Obj B) (f : Hom B a b ) -> |
| 249 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) ] | |
| 250 ≈ A [ FMap U f o id1 A (FObj U a) ] ] | |
| 251 lemma-nat1 a b f = let open ≈-Reasoning (A) in | |
| 252 begin | |
| 253 FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] ) o η (FObj U a) | |
| 254 ≈⟨ car ( IsFunctor.distr ( isFunctor U ) ) ⟩ | |
| 255 ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a) | |
| 256 ≈⟨ sym assoc ⟩ | |
| 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 ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 259 FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f ) | |
| 260 ≈⟨ assoc ⟩ | |
| 261 (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f | |
| 262 ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ | |
| 263 id1 A (FObj U b) o FMap U f | |
| 264 ≈⟨ idL ⟩ | |
| 265 FMap U f | |
| 266 ≈⟨ sym idR ⟩ | |
| 267 FMap U f o id (FObj U a) | |
| 268 ∎ | |
| 49 | 269 naturality : {a b : Obj B} {f : Hom B a b } |
| 270 → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ] | |
| 271 naturality {a} {b} {f} = let open ≈-Reasoning (B) in | |
| 272 sym ( begin | |
| 273 ε b o (FMap F' (FMap U f)) | |
| 274 ≈⟨⟩ | |
| 50 | 275 ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) |
| 276 ≈⟨⟩ | |
| 277 ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) | |
| 51 | 278 ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (FObj U a) b ) (lemma-nat1 a b f)) ⟩ |
| 279 (_* um) ( A [ FMap U f o id1 A (FObj U a) ] ) | |
| 49 | 280 ≈⟨ {!!} ⟩ |
| 50 | 281 f o ((_* um) ( id1 A (FObj U a))) |
| 282 ≈⟨⟩ | |
| 49 | 283 f o (ε a) |
| 284 ∎ ) | |
| 285 myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε | |
| 286 myIsNTrans = record { naturality = naturality } |