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

changeset 1284:45cd80181a29

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove import zf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 May 2023 09:48:37 +0900
parents f4dac8be0a01
children 302cfb533201
files src/BAlgebra.agda src/LEMC.agda src/OD.agda src/ODC.agda src/ODUtil.agda src/Ordinals.agda src/PFOD.agda src/Topology.agda src/Tychonoff.agda src/VL.agda src/ZProduct.agda src/cardinal.agda src/filter.agda src/generic-filter.agda src/maximum-filter.agda src/zorn.agda
diffstat 16 files changed, 41 insertions(+), 89 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/BAlgebra.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,7 @@
 open import Ordinals
 module BAlgebra {n : Level } (O : Ordinals {n})   where
 
-open import zf
+-- open import zf
 open import logic
 import OrdUtil
 import OD 
@@ -93,9 +93,9 @@
          A ∎ ) ox ) where open ≡-Reasoning
     ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox)
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
-    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
+    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) A
         ⟪ case1 refl , d→∋ A A∋x ⟫ )
-    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B
+    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) B
         ⟪ case2 refl , d→∋ B B∋x ⟫ )
 
 ∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
--- a/src/LEMC.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/LEMC.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Relation.Nullary
 module LEMC {n : Level } (O : Ordinals {n} )  where
 
-open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties 
--- a/src/OD.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/OD.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,7 +3,6 @@
 open import Ordinals
 module OD {n : Level } (O : Ordinals {n} ) where
 
-open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.Nat.Properties
@@ -108,6 +107,12 @@
 -- possible order restriction (required in the axiom of infinite )
   ho< : {x : HOD} → & x o< next (odmax x)
 
+-- sup-o may contradict
+--    If we have open monotonic function in Ordinal, there is no sup-o. 
+--    for example, if we may have countable sequence of Ordinal, which contains some ordinal larger than any given Ordinal.
+--    This happens when we have a coutable model. In this case, we have to have codomain restriction in  Replacement axiom.
+--    that is, Replacement axiom does not create new ZF set.
+
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
@@ -541,6 +546,8 @@
         ≡ & (Union (x , (x , x)))
     lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso
 
+open import zf
+
 isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
 isZF = record {
         isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
--- a/src/ODC.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/ODC.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,7 +3,6 @@
 open import Ordinals
 module ODC {n : Level } (O : Ordinals {n} ) where
 
-open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties
--- a/src/ODUtil.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/ODUtil.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,7 +3,6 @@
 open import Ordinals
 module ODUtil {n : Level } (O : Ordinals {n} ) where
 
-open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.Nat.Properties
--- a/src/Ordinals.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/Ordinals.agda	Sat May 20 09:48:37 2023 +0900
@@ -1,8 +1,6 @@
 open import Level
 module Ordinals where
 
-open import zf
-
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import  Relation.Binary.PropositionalEquality
--- a/src/PFOD.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/PFOD.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,7 +3,6 @@
 module PFOD {n : Level } (O : Ordinals {n})   where
 
 import filter 
-open import zf
 open import logic
 -- open import partfunc {n} O
 import OD 
--- a/src/Topology.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/Topology.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Ordinals
 module Topology {n : Level } (O : Ordinals {n})   where
 
-open import zf
 open import logic
 open _∧_
 open _∨_
--- a/src/Tychonoff.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/Tychonoff.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,7 +3,6 @@
 open import Ordinals
 module Tychonoff {n : Level } (O : Ordinals {n})   where
 
-open import zf
 open import logic
 open _∧_
 open _∨_
--- a/src/VL.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/VL.agda	Sat May 20 09:48:37 2023 +0900
@@ -2,7 +2,6 @@
 open import Ordinals
 module VL {n : Level } (O : Ordinals {n}) where
 
-open import zf
 open import logic
 import OD 
 open import Relation.Nullary 
--- a/src/ZProduct.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/ZProduct.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Ordinals
 module ZProduct {n : Level } (O : Ordinals {n})   where
 
-open import zf
 open import logic
 import OD
 import ODUtil
--- a/src/cardinal.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/cardinal.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Ordinals
 module cardinal {n : Level } (O : Ordinals {n}) where
 
-open import zf
 open import logic
 -- import OD
 import OD hiding ( _⊆_ )
@@ -43,41 +42,6 @@
 
 open HOD
 
--- _⊗_ : (A B : HOD) → HOD
--- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
-
-record Func (A B : HOD) : Set n where
-    field
-       func : Ordinal → Ordinal
-       is-func : {x : Ordinal } → odef A x → odef B (func x)
-
-data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
-     felm :  (F : Func A B) → FuncHOD A B (& ( Replace A ( λ x → < x , (* (Func.func F (& x))) > )))
-
-FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
-FuncHOD→F {A} {B} (felm F) = F
-
-FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
-FuncHOD=R {A} {B}  (felm F) = *iso
-
---
---  Set of All function from A to B
---
-Funcs : (A B : HOD) → HOD
-Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B)) 
-       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
-    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (A ⊗ B) x
-    lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
-    ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (A ⊗ B) k ) (sym x=ψz) (
-       product→ (subst (λ k → odef A k) (sym &iso) az) (subst (λ k → odef B k) 
-         (trans (cong (Func.func F) (sym &iso)) (sym &iso)) (Func.is-func F az) ))
-
-record Injection (A B : Ordinal ) : Set n where
-   field
-       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
-       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
-       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
-
 record OrdBijection (A B : Ordinal ) : Set n where
    field
        fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
--- a/src/filter.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/filter.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Ordinals
 module filter {n : Level } (O : Ordinals {n})   where
 
-open import zf
 open import logic
 import OD 
 
--- a/src/generic-filter.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/generic-filter.agda	Sat May 20 09:48:37 2023 +0900
@@ -3,10 +3,7 @@
 open import Ordinals
 module generic-filter {n : Level.Level } (O : Ordinals {n})   where
 
--- import filter
-open import zf
 open import logic
--- open import partfunc {n} O
 import OD
 
 open import Relation.Nullary
@@ -82,16 +79,16 @@
        cod-iso← : { x : ℕ } → cod← (cod→ x) ≡ x
        -- Since it is countable, it is HOD.
 
-CM : COD → CountableModel 
-CM cod = record { 
-       ctl-M = ?
-     ; ctl→ = λ n → ?
-     ; ctl<M = λ n → ?
-     ; ctl← = λ x → ?
-     ; ctl-iso→ = ?
-     ; TC = ?
-     ; is-model = ?
-       }
+-- CM : COD → CountableModel 
+-- CM cod = record { 
+--       ctl-M = ?
+--     ; ctl→ = λ n → ?
+--     ; ctl<M = λ n → ?
+--     ; ctl← = λ x → ?
+--     ; ctl-iso→ = ?
+--     ; TC = ?
+--     ; is-model = ?
+--       }
 
 open CountableModel
 
@@ -424,23 +421,23 @@
 GH : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
       → (C : CountableModel ) → HOD
 GH P L p0 LPP Lp0 C = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
-
-module _ {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (GF : GenericFilter {L} {P} LP M) where
-
-    MG = MG1 {L} {P} LP M GF 
-    G = ⊆-Ideal.ideal (genf GF)
-
-    M⊆MG : M ⊆ MG 
-    M⊆MG = case1
-
-    MG∋G : MG ∋ G
-    MG∋G = case2 record { owner = ? ; ao = ? ; ox = ? } where
-       gf00 : ?
-       gf00 = ?
-
-    MG∋UG : MG ∋ Union G
-    MG∋UG = case2 record { owner = ? ; ao = ? ; ox = ? } where
-       gf00 : ?
-       gf00 = ?
-
-
+-- 
+-- module _ {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (GF : GenericFilter {L} {P} LP M) where
+-- 
+--     MG = MG1 {L} {P} LP M GF 
+--     G = ⊆-Ideal.ideal (genf GF)
+-- 
+--     M⊆MG : M ⊆ MG 
+--     M⊆MG = case1
+-- 
+--     MG∋G : MG ∋ G
+--     MG∋G = case2 record { owner = ? ; ao = ? ; ox = ? } where
+--        gf00 : ?
+--        gf00 = ?
+-- 
+--     MG∋UG : MG ∋ Union G
+--     MG∋UG = case2 record { owner = ? ; ao = ? ; ox = ? } where
+--        gf00 : ?
+--        gf00 = ?
+-- 
+-- 
--- a/src/maximum-filter.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/maximum-filter.agda	Sat May 20 09:48:37 2023 +0900
@@ -4,7 +4,6 @@
 open import Ordinals
 module maximum-filter {n : Level } (O : Ordinals {n})   where
 
-open import zf
 open import logic
 import OD 
 
--- a/src/zorn.agda	Sat May 13 10:53:32 2023 +0900
+++ b/src/zorn.agda	Sat May 20 09:48:37 2023 +0900
@@ -14,9 +14,7 @@
 --     → Maximal A
 --
 
-open import zf -- hiding ( _⊆_ )
 open import logic
--- open import partfunc {n} O
 
 open import Relation.Nullary
 open import Data.Empty
@@ -26,7 +24,6 @@
 open import Data.Nat.Properties
 open import nat
 
-
 open inOrdinal O
 open OD O
 open OD.OD
@@ -39,7 +36,6 @@
 open OrdUtil O
 open ODUtil O
 
-
 import ODC
 
 open _∧_