Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 428:94392feeebc5
add Topology
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 19 Dec 2020 21:43:21 +0900 |
| parents | 9b0630f03c4b |
| children | 8d8149bcd4d1 |
| files | OD.agda ODUtil.agda OrdUtil.agda Topology.agda cardinal.agda generic-filter.agda logic.agda zf.agda |
| diffstat | 8 files changed, 103 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Sat Aug 08 18:14:14 2020 +0900 +++ b/OD.agda Sat Dec 19 21:43:21 2020 +0900 @@ -9,8 +9,8 @@ open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.Core +open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core hiding (_⇔_) open import logic import OrdUtil @@ -50,7 +50,7 @@ ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } -⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y +⇔→== : { x y : OD } → ( {z : Ordinal } → (def x z ⇔ def y z)) → x == y eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m
--- a/ODUtil.agda Sat Aug 08 18:14:14 2020 +0900 +++ b/ODUtil.agda Sat Dec 19 21:43:21 2020 +0900 @@ -9,8 +9,7 @@ open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.Core +open import Relation.Binary hiding ( _⇔_ ) open import logic open import nat
--- a/OrdUtil.agda Sat Aug 08 18:14:14 2020 +0900 +++ b/OrdUtil.agda Sat Dec 19 21:43:21 2020 +0900 @@ -8,7 +8,7 @@ open import Data.Empty open import Relation.Binary.PropositionalEquality open import Relation.Nullary -open import Relation.Binary +open import Relation.Binary hiding (_⇔_) open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal @@ -283,5 +283,5 @@ trans1 --<-transˡ trans2 --<-transʳ public - hiding (_≈⟨_⟩_) + -- hiding (_≈⟨_⟩_)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Topology.agda Sat Dec 19 21:43:21 2020 +0900 @@ -0,0 +1,91 @@ +open import Level +open import Ordinals +module Topology {n : Level } (O : Ordinals {n}) where + +open import zf +open import logic +open _∧_ +open _∨_ +open Bool + +import OD +open import Relation.Nullary +open import Data.Empty +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +import BAlgbra +open BAlgbra O +open inOrdinal O +open OD O +open OD.OD +open ODAxiom odAxiom +import OrdUtil +import ODUtil +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +open Ordinals.IsNext isNext +open OrdUtil O +open ODUtil O + +import ODC +open ODC O + +open import filter + +record Toplogy ( L : HOD ) : Set (suc n) where + field + OS : HOD + OS⊆PL : OS ⊆ Power L + o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P + o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) + +open Toplogy + +record _covers_ ( P q : HOD ) : Set (suc n) where + field + cover : {x : HOD} → q ∋ x → HOD + P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt + isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x + +-- Base +-- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that +-- W ⊆ U ∩ V and x ∈ W . + +data genTop (P : HOD) : HOD → Set (suc n) where + gi : {x : HOD} → P ∋ x → genTop P x + g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y) + g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q) + +-- Limit point + +record LP ( L S x : HOD ) (top : Toplogy L) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where + field + neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD + isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x ) + +-- Finite Intersection Property + +data Finite-∩ (S : HOD) : HOD → Set (suc n) where + fin-∩e : {x : HOD} → S ∋ x → Finite-∩ S x + fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y) + +data Finite-∪ (S : HOD) : HOD → Set (suc n) where + fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x + fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y) + +record FIP ( L : HOD ) : Set (suc n) where + field + fipS : HOD + fipS⊆PL : fipS ⊆ Power L + fip≠φ : { x : HOD } → Finite-∩ fipS x → ¬ ( x ≡ od∅ ) + +-- Compact + +record Compact ( L P : HOD ) : Set (suc n) where + field + finCover : {X y : HOD} → X covers P → P ∋ y → HOD + isFinCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y + isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y ) + + +-- Product Topology
--- a/cardinal.agda Sat Aug 08 18:14:14 2020 +0900 +++ b/cardinal.agda Sat Dec 19 21:43:21 2020 +0900 @@ -83,7 +83,7 @@ cmax : (x : Ordinal) → card o< x → ¬ Bijection a x Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t -Cardinal∈ = ? +Cardinal∈ = {!!} Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t ) Cardinal⊆ = {!!}
--- a/generic-filter.agda Sat Aug 08 18:14:14 2020 +0900 +++ b/generic-filter.agda Sat Dec 19 21:43:21 2020 +0900 @@ -140,7 +140,8 @@ open _==_ -postulate f-extensionality : { n m : Level} → Relation.Binary.PropositionalEquality.Extensionality n m +import Axiom.Extensionality.Propositional +postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f ω2∋f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt)) @@ -219,7 +220,7 @@ -- PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD PDHOD C P = record { od = record { def = λ x → PDN C P x } - ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) } where + ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt) } open PDN