Mercurial > hg > Members > kono > Proof > category
annotate pullback.agda @ 303:7f40d6a51c72
Limit form equalizer and product done.
Use equalizer to provle naturality of limit-ε
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 Nov 2013 14:46:07 +0900 |
| parents | c5b2656dbec6 |
| children | 702adc45704f |
| rev | line source |
|---|---|
| 260 | 1 -- Pullback from product and equalizer |
| 2 -- | |
| 3 -- | |
| 4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 5 ---- | |
| 6 | |
| 7 open import Category -- https://github.com/konn/category-agda | |
| 8 open import Level | |
| 266 | 9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where |
| 260 | 10 |
| 11 open import HomReasoning | |
| 12 open import cat-utility | |
| 13 | |
| 282 | 14 -- |
| 264 | 15 -- Pullback from equalizer and product |
| 260 | 16 -- f |
| 300 | 17 -- a ------→ c |
| 282 | 18 -- ^ ^ |
| 260 | 19 -- π1 | |g |
| 20 -- | | | |
| 300 | 21 -- ab ------→ b |
| 260 | 22 -- ^ π2 |
| 23 -- | | |
| 282 | 24 -- | e = equalizer (f π1) (g π1) |
| 264 | 25 -- | |
| 26 -- d <------------------ d' | |
| 27 -- k (π1' × π2' ) | |
| 260 | 28 |
| 261 | 29 open Equalizer |
| 30 open Product | |
| 31 open Pullback | |
| 32 | |
| 282 | 33 pullback-from : (a b c ab d : Obj A) |
| 260 | 34 ( f : Hom A a c ) ( g : Hom A b c ) |
| 261 | 35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) |
| 282 | 36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) |
| 37 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g | |
| 261 | 38 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) |
| 282 | 39 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) |
| 261 | 40 pullback-from a b c ab d f g π1 π2 e eqa prod = record { |
| 260 | 41 commute = commute1 ; |
| 282 | 42 p = p1 ; |
| 43 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; | |
| 44 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; | |
| 260 | 45 uniqueness = uniqueness1 |
| 282 | 46 } where |
| 302 | 47 commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] |
| 48 ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] | |
| 262 | 49 commute1 = let open ≈-Reasoning (A) in |
| 50 begin | |
| 282 | 51 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) |
| 262 | 52 ≈⟨ assoc ⟩ |
| 282 | 53 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) |
| 262 | 54 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ |
| 282 | 55 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) |
| 262 | 56 ≈↑⟨ assoc ⟩ |
| 282 | 57 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) |
| 262 | 58 ∎ |
| 282 | 59 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → |
| 262 | 60 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] |
| 282 | 61 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in |
| 262 | 62 begin |
| 63 ( f o π1 ) o (prod × π1') π2' | |
| 64 ≈↑⟨ assoc ⟩ | |
| 65 f o ( π1 o (prod × π1') π2' ) | |
| 66 ≈⟨ cdr (π1fxg=f prod) ⟩ | |
| 67 f o π1' | |
| 68 ≈⟨ eq ⟩ | |
| 69 g o π2' | |
| 70 ≈↑⟨ cdr (π2fxg=g prod) ⟩ | |
| 71 g o ( π2 o (prod × π1') π2' ) | |
| 72 ≈⟨ assoc ⟩ | |
| 73 ( g o π2 ) o (prod × π1') π2' | |
| 74 ∎ | |
| 261 | 75 p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d |
| 282 | 76 p1 {d'} { π1' } { π2' } eq = |
| 262 | 77 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) |
| 282 | 78 π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
| 262 | 79 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] |
| 80 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in | |
| 81 begin | |
| 82 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
| 83 ≈⟨⟩ | |
| 84 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
| 85 ≈↑⟨ assoc ⟩ | |
| 86 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
| 87 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
| 282 | 88 π1 o (_×_ prod π1' π2' ) |
| 262 | 89 ≈⟨ π1fxg=f prod ⟩ |
| 90 π1' | |
| 91 ∎ | |
| 282 | 92 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
| 263 | 93 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] |
| 262 | 94 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in |
| 95 begin | |
| 96 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
| 97 ≈⟨⟩ | |
| 98 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
| 99 ≈↑⟨ assoc ⟩ | |
| 100 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
| 101 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
| 282 | 102 π2 o (_×_ prod π1' π2' ) |
| 262 | 103 ≈⟨ π2fxg=g prod ⟩ |
| 104 π2' | |
| 105 ∎ | |
| 302 | 106 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} |
| 107 {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → | |
| 261 | 108 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → |
| 109 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → | |
| 110 A [ p1 eq ≈ p' ] | |
| 264 | 111 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in |
| 263 | 112 begin |
| 113 p1 eq | |
| 114 ≈⟨⟩ | |
| 115 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
| 264 | 116 ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin |
| 117 e o p' | |
| 118 ≈⟨⟩ | |
| 119 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' | |
| 120 ≈↑⟨ Product.uniqueness prod ⟩ | |
| 121 (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) | |
| 122 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ | |
| 123 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) | |
| 282 | 124 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) |
| 264 | 125 ≈⟨ ×-cong prod eq1 eq2 ⟩ |
| 126 ((prod × π1') π2') | |
| 127 ∎ ) ⟩ | |
| 263 | 128 p' |
| 129 ∎ | |
| 130 | |
| 266 | 131 ------ |
| 132 -- | |
| 133 -- Limit | |
| 134 -- | |
| 135 ----- | |
| 136 | |
| 137 -- Constancy Functor | |
| 138 | |
| 291 | 139 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) |
| 140 → ( a : Obj A ) → Functor I A | |
| 141 K A I a = record { | |
| 265 | 142 FObj = λ i → a ; |
| 143 FMap = λ f → id1 A a ; | |
| 144 isFunctor = let open ≈-Reasoning (A) in record { | |
| 145 ≈-cong = λ f=g → refl-hom | |
| 146 ; identity = refl-hom | |
| 147 ; distr = sym idL | |
| 148 } | |
| 149 } | |
| 150 | |
| 151 open NTrans | |
| 152 | |
| 291 | 153 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) |
| 154 ( a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 265 | 155 field |
| 291 | 156 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0 |
| 157 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } → | |
| 265 | 158 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] |
| 291 | 159 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → |
| 271 | 160 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
161 A0 : Obj A |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
162 A0 = a0 |
| 291 | 163 T0 : NTrans I A ( K A I a0 ) Γ |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
164 T0 = t0 |
| 265 | 165 |
| 266 | 166 -------------------------------- |
| 167 -- | |
| 168 -- If we have two limits on c and c', there are isomorphic pair h, h' | |
| 169 | |
| 170 open Limit | |
| 171 | |
| 172 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
| 291 | 173 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
| 174 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) | |
| 266 | 175 → Hom A a0 a0' |
| 176 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0 | |
| 177 | |
| 178 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
| 291 | 179 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
| 180 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) | |
| 266 | 181 → Hom A a0' a0 |
| 182 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0' | |
| 183 | |
| 184 | |
| 185 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
| 291 | 186 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
| 187 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } → | |
| 266 | 188 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ] |
| 189 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin | |
| 190 limit lim' a0 t0 o limit lim a0' t0' | |
| 271 | 191 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin |
| 266 | 192 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' ) |
| 193 ≈⟨ assoc ⟩ | |
| 282 | 194 ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0' |
| 266 | 195 ≈⟨ car ( t0f=t lim' ) ⟩ |
| 282 | 196 TMap t0 i o limit lim a0' t0' |
| 266 | 197 ≈⟨ t0f=t lim ⟩ |
| 282 | 198 TMap t0' i |
| 271 | 199 ∎) ) ⟩ |
| 266 | 200 limit lim' a0' t0' |
| 271 | 201 ≈⟨ limit-uniqueness lim' idR ⟩ |
| 266 | 202 id a0' |
| 203 ∎ | |
| 204 | |
| 205 | |
| 282 | 206 open import CatExponetial |
| 267 | 207 |
| 208 open Functor | |
| 209 | |
| 210 -------------------------------- | |
| 211 -- | |
| 212 -- Contancy Functor | |
| 266 | 213 |
| 268 | 214 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) |
| 215 KI { c₁'} {c₂'} {ℓ'} I = record { | |
| 291 | 216 FObj = λ a → K A I a ; |
| 217 FMap = λ f → record { -- NTrans I A (K A I a) (K A I b) | |
| 267 | 218 TMap = λ a → f ; |
| 282 | 219 isNTrans = record { |
| 267 | 220 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f |
| 221 } | |
| 282 | 222 } ; |
| 266 | 223 isFunctor = let open ≈-Reasoning (A) in record { |
| 267 | 224 ≈-cong = λ f=g {x} → f=g |
| 266 | 225 ; identity = refl-hom |
| 267 | 226 ; distr = refl-hom |
| 266 | 227 } |
| 267 | 228 } where |
| 229 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) → | |
| 291 | 230 A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ] |
| 282 | 231 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin |
| 291 | 232 FMap (K A I b') f₁ o f |
| 267 | 233 ≈⟨ idL ⟩ |
| 234 f | |
| 235 ≈↑⟨ idR ⟩ | |
| 291 | 236 f o FMap (K A I a') f₁ |
| 267 | 237 ∎ |
| 238 | |
| 239 | |
| 272 | 240 --------- |
| 241 -- | |
| 298 | 242 -- Limit Constancy Functor F : A → A^I has right adjoint |
| 243 -- | |
| 244 -- we are going to prove universal mapping | |
| 245 | |
| 246 --------- | |
| 247 -- | |
| 272 | 248 -- limit gives co universal mapping ( i.e. adjunction ) |
| 249 -- | |
| 250 -- F = KI I : Functor A (A ^ I) | |
| 282 | 251 -- U = λ b → A0 (lim b {a0 b} {t0 b} |
| 252 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) | |
| 272 | 253 |
| 282 | 254 limit2couniv : |
| 291 | 255 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) |
| 256 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b ) | |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
257 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) |
| 277 | 258 limit2couniv lim a0 t0 = record { -- F U ε |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
259 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
260 iscoUniversalMapping = record { |
| 282 | 261 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; |
| 271 | 262 couniquness = couniquness2 |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
263 } |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
264 } where |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
265 couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} → |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
266 A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ] |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
267 couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin |
| 282 | 268 TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
269 ≈⟨⟩ |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
270 TMap (t0 b) i o (limit (lim b) a f) |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
271 ≈⟨ t0f=t (lim b) ⟩ |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
272 TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ] |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
273 ∎ |
| 271 | 274 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} → |
| 282 | 275 ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] ) |
| 272 | 276 → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ] |
| 271 | 277 couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
278 limit (lim b {a0 b} {t0 b} ) a f |
| 271 | 279 ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩ |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
280 g |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
281 ∎ |
| 268 | 282 |
| 272 | 283 open import Category.Cat |
| 275 | 284 |
| 285 | |
| 278 | 286 open coUniversalMapping |
| 282 | 287 |
| 288 univ2limit : | |
| 289 ( U : Obj (A ^ I ) → Obj A ) | |
| 291 | 290 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b ) |
|
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
291 ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) → |
| 291 | 292 ( Γ : Functor I A ) → Limit A I Γ (U Γ) (ε Γ) |
| 278 | 293 univ2limit U ε univ Γ = record { |
| 272 | 294 limit = λ a t → limit1 a t ; |
| 282 | 295 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; |
| 296 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
| 272 | 297 } where |
| 291 | 298 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ) |
| 282 | 299 limit1 a t = _*' univ {_} {a} t |
| 291 | 300 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → |
|
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
301 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ] |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
302 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
|
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
303 TMap (ε Γ) i o limit1 a t |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
304 ≈⟨⟩ |
| 280 | 305 TMap (ε Γ) i o _*' univ {Γ} {a} t |
| 306 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩ | |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
307 TMap t i |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
308 ∎ |
| 291 | 309 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)} |
|
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
310 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
311 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin |
| 278 | 312 _*' univ t |
| 313 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ | |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
314 f |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
315 ∎ |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
316 |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
317 |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
318 lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) → |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
319 A [ _×_ prod π1 π2 ≈ id1 A ab ] |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
320 lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
321 _×_ prod π1 π2 |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
322 ≈↑⟨ ×-cong prod idR idR ⟩ |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
323 _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ]) |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
324 ≈⟨ Product.uniqueness prod ⟩ |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
325 id1 A ab |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
326 ∎ |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
327 |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
328 |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
329 ----- |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
330 -- |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
331 -- product on arbitrary index |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
332 -- |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
333 |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
334 record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
335 ( p : Obj A ) -- product |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
336 ( ai : I → Obj A ) -- families |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
337 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
338 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
339 field |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
340 product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
341 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ] |
|
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
342 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] |
| 283 | 343 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } |
| 282 | 344 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] |
| 302 | 345 -- another form of uniquness |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
346 ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) |
| 302 | 347 → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
348 → A [ product' ≈ product qi ] |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
349 ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin |
| 302 | 350 product' |
| 351 ≈↑⟨ ip-uniqueness ⟩ | |
| 352 product (λ i₁ → A [ pi i₁ o product' ]) | |
| 353 ≈⟨ ip-cong ( λ i → begin | |
| 354 pi i o product' | |
| 355 ≈⟨ eq {i} ⟩ | |
| 356 qi i | |
| 357 ∎ ) ⟩ | |
| 358 product qi | |
| 359 ∎ | |
| 282 | 360 |
| 361 open IProduct | |
| 283 | 362 open Equalizer |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
363 |
| 282 | 364 -- |
| 365 -- limit from equalizer and product | |
| 366 -- | |
| 367 -- | |
| 283 | 368 -- ai |
| 369 -- ^ K f = id lim | |
| 300 | 370 -- | pi lim = K i -----------→ K j = lim |
| 283 | 371 -- | | | |
| 372 -- p | | | |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
373 -- ^ proj i o e = ε i | | ε j = proj j o e |
| 283 | 374 -- | | | |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
375 -- | e = equalizer (id p) (id p) | | |
| 283 | 376 -- | v v |
| 300 | 377 -- lim <------------------ d' a i = Γ i -----------→ Γ j = a j |
| 283 | 378 -- k ( product pi ) Γ f |
| 379 -- Γ f o ε i = ε j | |
| 380 -- | |
| 291 | 381 |
| 283 | 382 limit-ε : |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
383 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) |
| 282 | 384 ( lim p : Obj A ) ( e : Hom A lim p ) |
| 385 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → | |
| 291 | 386 NTrans I A (K A I lim) Γ |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
387 limit-ε eqa lim p e proj = record { |
| 282 | 388 TMap = tmap ; |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
389 isNTrans = record { commute = commute1 } |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
390 } where |
| 291 | 391 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
392 tmap i = A [ proj i o e ] |
| 283 | 393 commute1 : {i j : Obj I} {f : Hom I i j} → |
| 291 | 394 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ] |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
395 commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
396 FMap Γ f o tmap i |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
397 ≈⟨⟩ |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
398 FMap Γ f o ( proj i o e ) |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
399 ≈⟨ assoc ⟩ |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
400 ( FMap Γ f o proj i ) o e |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
401 ≈⟨ fe=ge ( eqa e (FMap Γ f o proj i) ( proj j )) ⟩ |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
402 proj j o e |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
403 ≈↑⟨ idR ⟩ |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
404 (proj j o e ) o id1 A lim |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
405 ≈⟨⟩ |
| 291 | 406 tmap j o FMap (K A I lim) f |
| 288 | 407 ∎ |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
408 |
| 282 | 409 limit-from : |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
410 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
411 → IProduct {c₁'} A (Obj I) p ai pi ) |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
412 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) |
| 290 | 413 ( lim p : Obj A ) -- limit to be made |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
414 ( e : Hom A lim p ) -- existing of equalizer |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
415 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
416 → Limit A I Γ lim ( limit-ε eqa lim p e proj ) |
| 290 | 417 limit-from prod eqa lim p e proj = record { |
| 282 | 418 limit = λ a t → limit1 a t ; |
| 419 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
| 420 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
| 421 } where | |
| 291 | 422 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim |
| 283 | 423 limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom |
| 291 | 424 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
425 A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ] |
| 283 | 426 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
427 TMap (limit-ε eqa lim p e proj ) i o limit1 a t |
| 283 | 428 ≈⟨⟩ |
| 429 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom | |
| 430 ≈↑⟨ assoc ⟩ | |
| 431 proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) | |
| 432 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ | |
| 433 proj i o product (prod p (FObj Γ) proj) (TMap t) | |
| 434 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ | |
| 435 TMap t i | |
| 436 ∎ | |
| 291 | 437 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
438 → ({i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o f ] ≈ TMap t i ]) → |
| 282 | 439 A [ limit1 a t ≈ f ] |
| 283 | 440 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin |
| 441 limit1 a t | |
| 442 ≈⟨⟩ | |
| 443 k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom | |
| 444 ≈⟨ Equalizer.uniqueness (eqa e (id1 A p) (id1 A p )) ( begin | |
| 445 e o f | |
| 446 ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩ | |
| 447 product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) ) | |
| 284 | 448 ≈⟨ ip-cong (prod p (FObj Γ) proj) ( λ i → begin |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
449 proj i o ( e o f ) |
| 284 | 450 ≈⟨ assoc ⟩ |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
451 ( proj i o e ) o f |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
452 ≈⟨ lim=t {i} ⟩ |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
453 TMap t i |
| 284 | 454 ∎ ) ⟩ |
| 283 | 455 product (prod p (FObj Γ) proj) (TMap t) |
| 456 ∎ ) ⟩ | |
| 457 f | |
| 458 ∎ | |
| 459 | |
| 291 | 460 ---- |
| 461 -- | |
| 462 -- Adjoint functor preserves limits | |
| 463 -- | |
| 464 -- | |
| 465 | |
| 466 open import Category.Cat | |
| 467 | |
| 468 ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
469 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → |
| 291 | 470 ( U : Functor B A) → NTrans I A ( K A I (FObj U lim) ) (U ○ Γ) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
471 ta1 B Γ lim tb U = record { |
| 291 | 472 TMap = TMap (Functor*Nat I A U tb) ; |
| 473 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin | |
| 474 FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a | |
| 475 ≈⟨ nat ( Functor*Nat I A U tb ) ⟩ | |
| 476 TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f | |
| 477 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ | |
| 478 TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f | |
| 479 ∎ | |
| 480 } } | |
| 481 | |
| 482 adjoint-preseve-limit : | |
| 483 { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
484 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limitb : Limit B I Γ lim tb ) → |
| 291 | 485 { U : Functor B A } { F : Functor A B } |
| 293 | 486 { η : NTrans A A identityFunctor ( U ○ F ) } |
| 291 | 487 { ε : NTrans B B ( F ○ U ) identityFunctor } → |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
488 ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb U ) |
| 292 | 489 adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record { |
| 291 | 490 limit = λ a t → limit1 a t ; |
| 491 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
| 492 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
| 493 } where | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
494 ta = ta1 B Γ lim tb U |
| 293 | 495 tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i) |
| 496 tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] | |
| 497 tF : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → NTrans I B (K B I (FObj F a)) Γ | |
| 498 tF a t = record { | |
| 499 TMap = tfmap a t ; | |
| 500 isNTrans = record { commute = λ {a'} {b} {f} → let open ≈-Reasoning (B) in begin | |
| 501 FMap Γ f o tfmap a t a' | |
| 294 | 502 ≈⟨⟩ |
| 503 FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a')) | |
| 504 ≈⟨ assoc ⟩ | |
| 505 (FMap Γ f o TMap ε (FObj Γ a') ) o FMap F (TMap t a') | |
| 506 ≈⟨ car (nat ε) ⟩ | |
| 507 (TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a') | |
| 508 ≈↑⟨ assoc ⟩ | |
| 509 TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f) o FMap F (TMap t a') ) | |
| 510 ≈↑⟨ cdr ( distr F ) ⟩ | |
| 511 TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) ) | |
| 512 ≈⟨ cdr ( fcong F (nat t) ) ⟩ | |
| 513 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o FMap (K A I a) f ]) | |
| 514 ≈⟨⟩ | |
| 515 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ]) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
516 ≈⟨ cdr ( fcong F (idR1 A)) ⟩ |
| 294 | 517 TMap ε (FObj Γ b) o FMap F (TMap t b ) |
| 518 ≈↑⟨ idR ⟩ | |
| 519 ( TMap ε (FObj Γ b) o FMap F (TMap t b)) o id1 B (FObj F (FObj (K A I a) b)) | |
| 520 ≈⟨⟩ | |
| 293 | 521 tfmap a t b o FMap (K B I (FObj F a)) f |
| 522 ∎ | |
| 523 } } | |
| 524 limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim) | |
| 525 limit1 a t = A [ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ] | |
| 526 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} → | |
| 291 | 527 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ] |
| 295 | 528 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
| 529 TMap ta i o limit1 a t | |
| 530 ≈⟨⟩ | |
| 531 FMap U ( TMap tb i ) o ( FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ) | |
| 532 ≈⟨ assoc ⟩ | |
| 533 ( FMap U ( TMap tb i ) o FMap U (limit limitb (FObj F a) (tF a t ))) o TMap η a | |
| 534 ≈↑⟨ car ( distr U ) ⟩ | |
| 535 FMap U ( B [ TMap tb i o limit limitb (FObj F a) (tF a t ) ] ) o TMap η a | |
| 536 ≈⟨ car ( fcong U ( t0f=t limitb ) ) ⟩ | |
| 537 FMap U (TMap (tF a t) i) o TMap η a | |
| 538 ≈⟨⟩ | |
| 539 FMap U ( B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] ) o TMap η a | |
| 540 ≈⟨ car ( distr U ) ⟩ | |
| 541 ( FMap U ( TMap ε (FObj Γ i)) o FMap U ( FMap F (TMap t i) )) o TMap η a | |
| 542 ≈↑⟨ assoc ⟩ | |
| 543 FMap U ( TMap ε (FObj Γ i) ) o ( FMap U ( FMap F (TMap t i) ) o TMap η a ) | |
| 544 ≈⟨ cdr ( nat η ) ⟩ | |
| 545 FMap U (TMap ε (FObj Γ i)) o ( TMap η (FObj U (FObj Γ i)) o FMap (identityFunctor {_} {_} {_} {A}) (TMap t i) ) | |
| 546 ≈⟨ assoc ⟩ | |
| 547 ( FMap U (TMap ε (FObj Γ i)) o TMap η (FObj U (FObj Γ i))) o TMap t i | |
| 548 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ) ⟩ | |
| 549 id1 A (FObj (U ○ Γ) i) o TMap t i | |
| 550 ≈⟨ idL ⟩ | |
| 551 TMap t i | |
| 552 ∎ | |
| 296 | 553 -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i ) o f ≈ TMap t i |
| 293 | 554 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)} |
| 291 | 555 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) → |
| 556 A [ limit1 a t ≈ f ] | |
| 295 | 557 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin |
| 558 limit1 a t | |
| 559 ≈⟨⟩ | |
| 560 FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a | |
| 296 | 561 ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} → lemma1 i) )) ⟩ |
| 298 | 562 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a -- Universal mapping |
|
297
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
563 ≈⟨ car (distr U ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
564 ( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
565 ≈⟨ sym assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
566 (FMap U (TMap ε lim)) o ((FMap U ( FMap F f )) o TMap η a ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
567 ≈⟨ cdr (nat η) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
568 (FMap U (TMap ε lim)) o ((TMap η (FObj U lim )) o f ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
569 ≈⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
570 ((FMap U (TMap ε lim)) o (TMap η (FObj U lim))) o f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
571 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
572 id (FObj U lim) o f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
573 ≈⟨ idL ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
574 f |
| 296 | 575 ∎ where |
| 576 lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim o FMap F f ] ] ≈ TMap (tF a t) i ] | |
| 577 lemma1 i = let open ≈-Reasoning (B) in begin | |
| 578 TMap tb i o (TMap ε lim o FMap F f) | |
|
297
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
579 ≈⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
580 ( TMap tb i o TMap ε lim ) o FMap F f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
581 ≈⟨ car ( nat ε ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
582 ( TMap ε (FObj Γ i) o FMap F ( FMap U ( TMap tb i ))) o FMap F f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
583 ≈↑⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
584 TMap ε (FObj Γ i) o ( FMap F ( FMap U ( TMap tb i )) o FMap F f ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
585 ≈↑⟨ cdr ( distr F ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
586 TMap ε (FObj Γ i) o FMap F ( A [ FMap U ( TMap tb i ) o f ] ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
587 ≈⟨ cdr ( fcong F (lim=t {i}) ) ⟩ |
| 296 | 588 TMap ε (FObj Γ i) o FMap F (TMap t i) |
| 589 ≈⟨⟩ | |
| 590 TMap (tF a t) i | |
| 591 ∎ | |
| 295 | 592 |
| 296 | 593 |
| 594 |