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