Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 593:a158ebb391f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 May 2017 19:53:58 +0900
parents 0448a74c0a03
children db76b73b526c
comparison
equal deleted inserted replaced
592:0448a74c0a03 593:a158ebb391f2
178 178
179 record slim { c₂ } { I OC : Set c₂ } 179 record slim { c₂ } { I OC : Set c₂ }
180 ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) 180 ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j )
181 : Set c₂ where 181 : Set c₂ where
182 field 182 field
183 slequ : (i j : OC) (f : I → I ) → sequ (sproduct OC sobj) (sobj j) (λ x → smap f (proj x i) ) (λ x → proj x j ) 183 slproj : ( i : OC ) → sobj i
184 slequ : (i j : OC) (f : I → I ) → sequ OC (sobj j) (λ x → smap f (slproj i) ) (λ x → slproj j )
185 slprod : sproduct OC sobj
186 slprod = record { proj = slproj }
184 slmap : { i j : OC } → (f : I → I ) → sobj i → sobj j 187 slmap : { i j : OC } → (f : I → I ) → sobj i → sobj j
185 slmap f x = smap f x 188 slmap f x = smap f x
186 open slim 189 open slim
187 190
188 slprod : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
189 {i : Obj C } → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) → sproduct (Obj C) (ΓObj s Γ)
190 slprod C I s Γ {i} se = equ ( slequ se i i (slid C I s i ) )
191
192 open import HomReasoning 191 open import HomReasoning
193 open NTrans 192 open NTrans
194 193
195 llid : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 194
196 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) 195 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
197 → ( x : FObj Γ a ) 196 → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) Γ
198 → slmap se (slid C I s a ) x ≡ x 197 Cone {c₁} C I s Γ = record {
199 llid C I s Γ a b f se x = begin 198 TMap = λ i → λ se → proj ( slprod se ) i
200 slmap se (slid C I s a) x 199 ; isNTrans = record { commute = commute1 }
201 ≡⟨⟩ 200 } where
202 FMap Γ (hom← s (slid C I s a)) x 201 commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ] ≈
203 ≡⟨ ≡cong ( λ g → FMap Γ g x ) (hom-iso s ) ⟩ 202 Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
204 FMap Γ (id1 C a) x 203 commute1 {a} {b} {f} = extensionality Sets ( λ se → begin
205 ≡⟨ ≡cong ( λ g → g x ) ( IsFunctor.identity (isFunctor Γ ) ) ⟩ 204 FMap Γ f (proj (slprod se ) a )
206 x 205 ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod se) a)) (sym ( hom-iso s ) ) ⟩
207 ∎ where 206 FMap Γ (hom← s ( hom→ s f)) (proj (slprod se) a)
208 open import Relation.Binary.PropositionalEquality 207 ≡⟨ fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
209 open ≡-Reasoning 208 proj (slprod se) b
210
211
212 lldistr : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
213 → (a b c : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
214 → ( x : FObj Γ a )
215 → slmap se {a} {c} ( λ y → f ( g y )) x ≡ slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
216 lldistr C I s Γ a b c f g se x = begin
217 slmap se {a} {c} ( λ y → f ( g y )) x
218 ≡⟨⟩
219 FMap Γ (hom← s (λ y → f (g y))) x
220 ≡⟨ ? ⟩
221 FMap Γ (hom← s (λ y → f ( hom→ s ( hom← s g) y ))) x
222 ≡⟨ {!!} ⟩
223 FMap Γ (C [ hom← s f o hom← s g ]) x
224 ≡⟨ ≡cong ( λ g → g x ) ( IsFunctor.distr (isFunctor Γ ) ) ⟩
225 (Sets [ FMap Γ (hom← s f) o FMap Γ (hom← s g ) ]) x
226 ≡⟨⟩
227 slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
228 ∎ where
229 open import Relation.Binary.PropositionalEquality
230 open ≡-Reasoning
231
232
233 lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
234 {i j i' j' : Obj C } →　 { f f' : I → I }
235 → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
236 → proj (equ (slequ se i j f)) i ≡ proj (equ (slequ se i' j' f' )) i
237 lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se = ≡cong ( λ p -> proj p i ) ( begin
238 equ (slequ se i j f )
239 ≡⟨⟩
240 record { proj = λ x → proj (equ (slequ se i j f)) x }
241 ≡⟨ ≡cong ( λ p → record { proj = proj p i }) ( ≡cong ( λ QIX → record { proj = QIX } ) (
242 extensionality Sets ( λ x → ≡cong ( λ qi →　qi x ) refl
243 ) )) ⟩
244 record { proj = λ x → proj (equ (slequ se i' j' f')) x }
245 ≡⟨⟩
246 equ (slequ se i' j' f' )
247 ∎ ) where 209 ∎ ) where
248 open import Relation.Binary.PropositionalEquality 210 open import Relation.Binary.PropositionalEquality
249 open ≡-Reasoning 211 open ≡-Reasoning
250
251 llcomm : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
252 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
253 → proj ( equ ( slequ se a b f)) a ≡ slmap se f (proj (slprod C I s Γ {a} se ) a )
254 llcomm C I s Γ a b f se = begin
255 proj ( equ ( slequ se a b f)) a
256 ≡⟨ {!!} ⟩
257 slmap se f (proj (equ ( slequ se a a (slid C I s a))) a )
258 ≡⟨⟩
259 slmap se f (proj (slprod C I s Γ {a} se ) a )
260 ∎ where
261 open import Relation.Binary.PropositionalEquality
262 open ≡-Reasoning
263
264
265 lla : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
266 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
267 → proj ( equ ( slequ se a b f)) a ≡ proj (slprod C I s Γ {a} se ) a
268 lla C I s Γ a b f se = begin
269 proj ( equ ( slequ se a b f)) a
270 ≡⟨ {!!} ⟩
271 proj ( equ ( slequ se a a (slid C I s a))) a
272 ∎ where
273 open import Relation.Binary.PropositionalEquality
274 open ≡-Reasoning
275
276
277 llb : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
278 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
279 → proj ( equ ( slequ se a b f)) b ≡ proj (slprod C I s Γ {b} se ) b
280 llb C I s Γ a b f se = {!!}
281
282
283 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
284 → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ))) Γ
285 Cone {c₁} C I s Γ = record {
286 TMap = λ i → λ se → proj (slprod C I s Γ {i} se ) i
287 ; isNTrans = record { commute = commute1 }
288 } where
289 commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod C I s Γ {a} se ) a) ]
290 ≈ Sets [ (λ se → proj (slprod C I s Γ {b} se ) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
291 commute1 {a} {b} {f} = extensionality Sets ( λ se → begin
292 (Sets [ FMap Γ f o (λ se → proj (slprod C I s Γ {a} se ) a) ]) se
293 ≡⟨⟩
294 FMap Γ f (proj (slprod C I s Γ {a} se ) a )
295 ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod C I s Γ {a} se ) a)) (sym ( hom-iso s ) ) ⟩
296 FMap Γ (hom← s ( hom→ s f)) (proj (slprod C I s Γ {a} se ) a)
297 ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) (sym (lla C I s Γ a b ( hom→ s f) se ) ) ⟩
298 FMap Γ (hom← s ( hom→ s f)) (proj (equ ( slequ se a b ( hom→ s f))) a)
299 ≡⟨ fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
300 proj (equ (slequ se a b ( hom→ s f))) b
301 ≡⟨ llb C I s Γ a b ( hom→ s f) se ⟩
302 proj (slprod C I s Γ {b} se ) b
303 ≡⟨⟩
304 (Sets [ (λ se → proj (slprod C I s Γ {b} se ) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
305 ∎ ) where
306 open import Relation.Binary.PropositionalEquality
307 open ≡-Reasoning
308
309
310 212
311 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 213 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
312 → Limit Sets C Γ 214 → Limit Sets C Γ
313 SetsLimit { c₂} C I s Γ = record { 215 SetsLimit { c₂} C I s Γ = record {
314 a0 = slim (ΓObj s Γ) (ΓMap s Γ) 216 a0 = slim (ΓObj s Γ) (ΓMap s Γ)
315 ; t0 = Cone C I s Γ 217 ; t0 = Cone C I s Γ
316 ; isLimit = record { 218 ; isLimit = record {
317 limit = limit1 219 limit = limit1
318 ; t0f=t = λ {a t i } → {!!} 220 ; t0f=t = λ {a t i } → refl
319 ; limit-uniqueness = λ {a t i } → {!!} 221 ; limit-uniqueness = λ {a t f } → limit-uniqueness {a} {t} {f}
320 } 222 }
321 } where 223 } where
322 -- ( e : Obj C → sproduct (Obj C) sobj )
323 -- sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j)
324 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 224 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ))
325 limit1 a t = λ x → record { slequ = λ i j f → elem (record { proj = λ i → TMap t i x }) ( ≡cong ( λ g → g x) (IsNTrans.commute (isNTrans t ))) } 225 limit1 a t = λ x → record {
226 slequ = λ i j f → elem {!!} ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ))
227 ; slproj = λ i → ( TMap t i ) x
228 }
229 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ))} → ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
230 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
231 limit1 a t x
232 ≡⟨ {!!} ⟩
233 f x
234 ∎ ) where
235 open import Relation.Binary.PropositionalEquality
236 open ≡-Reasoning
237
238
239
240
241
242
243
244