Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1192:2c35ccd5aadd
...
| author | kono |
|---|---|
| date | Mon, 27 Feb 2023 13:13:15 +0800 |
| parents | d969fc17d049 |
| children | 8ea70b6effd4 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 5 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Mon Feb 27 08:26:35 2023 +0800 +++ b/src/Topology.agda Mon Feb 27 13:13:15 2023 +0800 @@ -358,7 +358,7 @@ fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 ) fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD - finCoverSet {X} x fin-e = ? + finCoverSet {X} x fin-e = od∅ finCoverSet {X} x (fin-i rx) = ( L ＼ * x ) , ( L ＼ * x ) finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy -- @@ -369,8 +369,10 @@ isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) - fip60 x fin-e = ? - fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) where + fip60 x fin-e = subst (λ k → Finite-∪ (* X) k) (sym ord-od∅) fin-e + fip60 x (fin-i {y} rx) = subst (λ k → Finite-∪ (* X) k) ? (fin-i ?) where + fip63 : odef (Replace (* X) (_＼_ L)) (& (* y , * y)) + fip63 = record { z = ? ; az = ? ; x=ψz = ? } fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) fip62 = cong₂ (λ j k → & (j , k )) *iso *iso fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))