Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/Topology.agda @ 1192:2c35ccd5aadd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Mon, 27 Feb 2023 13:13:15 +0800
parents d969fc17d049
children
comparison
equal deleted inserted replaced
1191:d969fc17d049 1192:2c35ccd5aadd
356 fip22 : odef (* (CX ox)) (& ( L ＼ * y )) 356 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
357 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } 357 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
358 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 ) 358 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
359 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) 359 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
360 finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD 360 finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD
361 finCoverSet {X} x fin-e = ? 361 finCoverSet {X} x fin-e = od∅
362 finCoverSet {X} x (fin-i rx) = ( L ＼ * x ) , ( L ＼ * x ) 362 finCoverSet {X} x (fin-i rx) = ( L ＼ * x ) , ( L ＼ * x )
363 finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 363 finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy
364 -- 364 --
365 -- this defines finite cover 365 -- this defines finite cover
366 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal 366 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
367 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) 367 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc))
368 -- create Finite-∪ from cex 368 -- create Finite-∪ from cex
369 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) 369 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
370 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where 370 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where
371 fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) 371 fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
372 fip60 x fin-e = ? 372 fip60 x fin-e = subst (λ k → Finite-∪ (* X) k) (sym ord-od∅) fin-e
373 fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) where 373 fip60 x (fin-i {y} rx) = subst (λ k → Finite-∪ (* X) k) ? (fin-i ?) where
374 fip63 : odef (Replace (* X) (_＼_ L)) (& (* y , * y))
375 fip63 = record { z = ? ; az = ? ; x=ψz = ? }
374 fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) 376 fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x))
375 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso 377 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso
376 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) )) 378 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))
377 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where 379 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
378 fip34 : * z1 ⊆ L 380 fip34 : * z1 ⊆ L