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

changeset 1124:d122d0c1b094

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Jan 2023 13:09:30 +0900
parents 256a3ba634f6
children edef8810a023
files src/BAlgbra.agda src/BAlgebra.agda src/PFOD.agda src/Topology.agda src/VL.agda src/cardinal.agda src/filter.agda src/generic-filter.agda src/zorn.agda
diffstat 9 files changed, 300 insertions(+), 234 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgbra.agda	Wed Jan 04 11:21:55 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-open import Level
-open import Ordinals
-module BAlgbra {n : Level } (O : Ordinals {n})   where
-
-open import zf
-open import logic
-import OrdUtil
-import OD 
-import ODUtil
-import ODC
-
-open import Relation.Nullary
-open import Relation.Binary
-open import Data.Empty
-open import Relation.Binary
-open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
-
-open inOrdinal O
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
-
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-open HOD
-
-open _∧_
-open _∨_
-open Bool
-
---_∩_ : ( A B : HOD  ) → HOD
---A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
---    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
-
-∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
-∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ =  λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
-
-_∪_ : ( A B : HOD  ) → HOD
-A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
-    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
-      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
-      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
-      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
-
-_＼_ : ( A B : HOD  ) → HOD
-A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
-
-¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
-¬∅∋ {x} = ¬x<0
-
-L＼L=0 : { L  : HOD  } → L ＼ L ≡ od∅ 
-L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← =  lem1 } ) where
-    lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
-    lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
-    lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
-    lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
-
-[a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
-[a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
-     ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
-
-U-F=∅→F⊆U : {F U : HOD} →  ((x : Ordinal) →  ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
-U-F=∅→F⊆U {F} {U} not = gt02  where
-    gt02 : { x : Ordinal } → odef F x → odef U x
-    gt02 {x} fx with ODC.∋-p O U (* x)
-    ... | yes y = subst (λ k → odef U k ) &iso y
-    ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
-
-∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
-∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
-    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
-    lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo )
-    ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin 
-         * owner ≡⟨ cong (*) (sym a=o)  ⟩ 
-         * (& A) ≡⟨ *iso ⟩ 
-         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
-        ⟪ 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
-        ⟪ case2 refl , d→∋ B B∋x ⟫ )
-
-∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
-∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
-    lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
-    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
-    lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
-
-dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
-dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
-    lemma1 {x} lt with proj2 lt
-    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ 
-    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ 
-    lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
-    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ 
-    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ 
-
-dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
-dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
-    lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
-    lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
-    lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
-    lemma2 {x} lt with proj1 lt | proj2 lt
-    lemma2 {x} lt | case1 cp | _ = case1 cp
-    lemma2 {x} lt | _ | case1 cp = case1 cp 
-    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
-
-record IsBooleanAlgebra ( L : Set n)
-       ( b1 : L )
-       ( b0 : L )
-       ( -_ : L → L  )
-       ( _+_ : L → L → L )
-       ( _x_ : L → L → L ) : Set (suc n) where
-   field
-       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
-       x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
-       +-sym : {a b : L } → a + b ≡ b + a
-       -sym : {a b : L } → a x b  ≡ b x a
-       +-aab : {a b : L } → a + ( a x b ) ≡ a
-       x-aab : {a b : L } → a x ( a + b ) ≡ a
-       +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
-       x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
-       a+0 : {a : L } → a + b0 ≡ a
-       ax1 : {a : L } → a x b1 ≡ a
-       a+-a1 : {a : L } → a + ( - a ) ≡ b1
-       ax-a0 : {a : L } → a x ( - a ) ≡ b0
-
-record BooleanAlgebra ( L : Set n) : Set (suc n) where
-   field
-       b1 : L
-       b0 : L
-       -_ : L → L 
-       _+_ : L → L → L
-       _x_ : L → L → L
-       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
-       
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/BAlgebra.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -0,0 +1,145 @@
+open import Level
+open import Ordinals
+module BAlgebra {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+import OrdUtil
+import OD 
+import ODUtil
+import ODC
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
+
+open inOrdinal O
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+open HOD
+
+open _∧_
+open _∨_
+open Bool
+
+--_∩_ : ( A B : HOD  ) → HOD
+--A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
+--    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
+
+∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
+∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ =  λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
+
+_∪_ : ( A B : HOD  ) → HOD
+A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
+    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
+      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
+      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
+      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
+
+_＼_ : ( A B : HOD  ) → HOD
+A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
+
+¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
+¬∅∋ {x} = ¬x<0
+
+L＼L=0 : { L  : HOD  } → L ＼ L ≡ od∅ 
+L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← =  lem1 } ) where
+    lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
+    lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
+    lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
+    lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+
+[a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
+[a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+     ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
+
+U-F=∅→F⊆U : {F U : HOD} →  ((x : Ordinal) →  ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
+U-F=∅→F⊆U {F} {U} not = gt02  where
+    gt02 : { x : Ordinal } → odef F x → odef U x
+    gt02 {x} fx with ODC.∋-p O U (* x)
+    ... | yes y = subst (λ k → odef U k ) &iso y
+    ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
+
+∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
+∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
+    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
+    lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo )
+    ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin 
+         * owner ≡⟨ cong (*) (sym a=o)  ⟩ 
+         * (& A) ≡⟨ *iso ⟩ 
+         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
+        ⟪ 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
+        ⟪ case2 refl , d→∋ B B∋x ⟫ )
+
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+    lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
+
+dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
+dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+    lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
+    lemma1 {x} lt with proj2 lt
+    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ 
+    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ 
+    lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
+    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ 
+    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ 
+
+dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
+dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+    lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
+    lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
+    lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
+    lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
+    lemma2 {x} lt with proj1 lt | proj2 lt
+    lemma2 {x} lt | case1 cp | _ = case1 cp
+    lemma2 {x} lt | _ | case1 cp = case1 cp 
+    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
+
+record IsBooleanAlgebra ( L : Set n)
+       ( b1 : L )
+       ( b0 : L )
+       ( -_ : L → L  )
+       ( _+_ : L → L → L )
+       ( _x_ : L → L → L ) : Set (suc n) where
+   field
+       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
+       x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
+       +-sym : {a b : L } → a + b ≡ b + a
+       -sym : {a b : L } → a x b  ≡ b x a
+       +-aab : {a b : L } → a + ( a x b ) ≡ a
+       x-aab : {a b : L } → a x ( a + b ) ≡ a
+       +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
+       x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
+       a+0 : {a : L } → a + b0 ≡ a
+       ax1 : {a : L } → a x b1 ≡ a
+       a+-a1 : {a : L } → a + ( - a ) ≡ b1
+       ax-a0 : {a : L } → a x ( - a ) ≡ b0
+
+record BooleanAlgebra ( L : Set n) : Set (suc n) where
+   field
+       b1 : L
+       b0 : L
+       -_ : L → L 
+       _+_ : L → L → L
+       _x_ : L → L → L
+       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
+       
--- a/src/PFOD.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/PFOD.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -15,9 +15,9 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra 
+import BAlgebra 
 
-open BAlgbra O
+open BAlgebra O
 
 open inOrdinal O
 open OD O
--- a/src/Topology.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/Topology.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -13,8 +13,8 @@
 open import Data.Empty
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
-import BAlgbra
-open BAlgbra O
+import BAlgebra
+open BAlgebra O
 open inOrdinal O
 open OD O
 open OD.OD
@@ -60,7 +60,7 @@
 
 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD
 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x  } 
-  ; odmax = & L ; <odmax = ? }
+  ; odmax = & L ; <odmax = {!!} }
 
 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L
 ClL {L} top {f} =  ==→o≡ ( record { eq→ = λ {x} ic 
@@ -203,37 +203,37 @@
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
    CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
    CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top 
-   CCX {X} ox = ?
+   CCX {X} ox = {!!}
    -- CX has finite intersection
    CXfip : {X : Ordinal } → * X ⊆ OS top → Set n
    CXfip {X} ox =  { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 
    Cex : {X : Ordinal } → * X ⊆ OS top → HOD
    Cex {X} ox =  record { od = record { def = λ C → { x : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) o∅ } 
-       ; odmax = osuc ( & (Power L)) ; <odmax = ? }
+       ; odmax = osuc ( & (Power L)) ; <odmax = {!!} }
    -- a counter example of fip , some CX has no finite intersection
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
    cex {X} ox oc = & ( ODC.minimal O (Cex ox) fip00)  where
       fip00 : ¬ ( Cex ox =h= od∅ ) 
-      fip00 cex=0 = fip03 ? ? where 
+      fip00 cex=0 = fip03 {!!} {!!} where 
           fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
           fip03 {x} {z} xz nxz = nxz xz
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
-          fip02 = ?
+          fip02 = {!!}
           fip01 : Ordinal
-          fip01 = FIP.limit fip (CCX ox) ? fip02
+          fip01 = FIP.limit fip (CCX ox) {!!} fip02
    ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 
-   ¬CXfip {X} ox oc = ? where
+   ¬CXfip {X} ox oc = {!!} where
       fip04 : odef (Cex ox) (cex ox oc)
-      fip04 = ?
+      fip04 = {!!}
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
    finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼  z ))
    -- create Finite-∪ from cex
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
-   isFinite = ?
+   isFinite = {!!}
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
-   isCover1 = ?
+   isCover1 = {!!}
 
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
@@ -287,7 +287,7 @@
 -- Ultra Filter has limit point
 
 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  
-      (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
+      (FL : filter F ∋ P) : Set (suc (suc n)) where
    field
        limit : Ordinal
        P∋limit : odef P limit
@@ -296,9 +296,11 @@
 -- FIP is UFL
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
-   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf
-FIP→UFLP {P} TP fip {L} LP F FP uf = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P)  → UFLP TP LP F FP 
+FIP→UFLP {P} TP fip {L} LP F FP = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
     where
+      uf : ultra-filter {L} {P} {LP} F
+      uf = {!!}
       fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
       fip03 {z} fz {x} zx = LP ( f⊆L F fz ) x (subst (λ k → odef k x) (sym *iso) zx  )
       CF : Ordinal
@@ -306,29 +308,36 @@
       CFP : * CF ∋ P  -- filter F ∋ P and Cl P ≡ P
       CFP = subst₂ (λ j k → odef j k) (sym *iso) refl record { z = & P ; az = FP ; x=ψz =  cong (&) fip04 }  where
            fip04 : P ≡ (Cl TP (* (& P)) (fip03 (subst (odef (filter F)) (sym &iso) FP)))
-           fip04 =  ==→o≡ ( record { eq→ = ? ;  eq← =  ?  } )
+           fip04 =  ==→o≡ ( record { eq→ = {!!} ;  eq← =  {!!}  } )
       fip00 : * CF ⊆ CS TP -- replaced
-      fip00 = ?
+      fip00 = {!!}
       fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x
-      fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅
-      fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ?
+      fip01 {C} {x} CCF (gi Cx) = {!!} -- filter is proper .i.e it contains no od∅
+      fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = {!!}
       fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 CFP fip01) → * o ⊆ filter F
-      fip02 {p} oo ol = ? where
-         fip04 : odef ? (FIP.limit fip fip00 CFP fip01) 
-         fip04 = FIP.is-limit fip fip00 CFP fip01 ?
+      fip02 {p} oo ol {x} ox = fip06 where
+         fip04 : odef {!!} (FIP.limit fip fip00 CFP fip01) 
+         fip04 = FIP.is-limit fip fip00 CFP fip01 {!!}
+         fip05 : ( filter F ∋ (* x) ) ∨ (  filter F ∋ ( P ＼ (* x))  )
+         fip05  = ultra-filter.ultra uf {!!} {!!} 
+         fip06 : odef (filter F) x
+         fip06 with fip05
+         ... | case1 lt = subst (λ k → odef (filter F) k ) &iso lt
+         ... | case2 nlt = {!!}
 
 
 UFLP→FIP : {P : HOD} (TP : Topology P) →
-   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf ) → FIP TP
-UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? }
+   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) → UFLP TP LP F FP ) → FIP TP
+UFLP→FIP {P} TP uflp = record { limit = {!!} ; is-limit = {!!} }
 
--- Product of UFL has limit point (Tychonoff)
+-- product topology of compact topology is compact
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (TP Top⊗ TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
+    -- Product of UFL has limit point 
     uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (LF : filter F ∋ ZFP P Q)
-            (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F ? uf
-    uflp {L} LPQ F LF uf = record { limit = & < * ( UFLP.limit uflpp) , ? >  ; P∋limit = ? ; is-limit = ? } where
+             → UFLP (TP Top⊗ TQ) LPQ F {!!} 
+    uflp {L} LPQ F LF = record { limit = & < * ( UFLP.limit uflpp) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
          LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD
          LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P
@@ -340,15 +349,13 @@
                     tp03 : odef (* z) z1 →  odef (* (& (* z))) (& (* z1))
                     tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
          FP : Filter (LPP L LPQ)
-         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where
+         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = {!!} ; filter2 = {!!} } where
              tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ
-             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? }
-         uFP : ultra-filter FP
-         uFP = record { proper = ? ; ultra = ? }
-         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP ? uFP
-         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP ? uFP
+             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = {!!} }
+         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP {!!} 
+         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP {!!} 
          LQ : HOD
          LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LQQ : LQ ⊆ Power Q
-         LQQ = ?
-
+         LQQ = {!!}
+-- S ⊆ ℕ 
--- a/src/VL.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/VL.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -12,8 +12,8 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra 
-open BAlgbra O
+import BAlgebra 
+open BAlgebra O
 open inOrdinal O
 import OrdUtil
 import ODUtil
--- a/src/cardinal.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/cardinal.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -60,7 +60,7 @@
        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 Bijection (A B : Ordinal ) : Set n where
+record OrdBijection (A B : Ordinal ) : Set n where
    field
        fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
        fun→  : (x : Ordinal ) → odef (* B)  x → Ordinal
@@ -69,8 +69,18 @@
        fiso← : (x : Ordinal ) → ( lt : odef (* B)  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
        fiso→ : (x : Ordinal ) → ( lt : odef (* A)  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
 
+ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
+ordbij-refl {a} refl = record {
+       fun←  = λ x _ → x 
+     ; fun→  = λ x _ → x 
+     ; funB  = λ x lt → lt
+     ; funA  = λ x lt → lt
+     ; fiso← = λ x lt → refl
+     ; fiso→ = λ x lt → refl
+    }
+
 open Injection
-open Bijection
+open OrdBijection
 
 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
    field
@@ -84,7 +94,7 @@
 image=a = ?
 
 _=c=_ : ( A B : HOD ) → Set n
-A =c= B = Bijection ( & A ) ( & B )
+A =c= B = OrdBijection ( & A ) ( & B )
 
 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
 c=→≡ = ?
@@ -92,24 +102,51 @@
 ≡→c= : {A B : HOD} → A ≡ B → A =c= B
 ≡→c= = ?
 
-Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b
-Bernstein {a} {b} iab iba = {!!} where
+open import BAlgebra O
+
+_-_ : (a b : Ordinal ) → Ordinal 
+a - b = & ( (* a) ＼ (* b) )
+
+-→<  : (a b : Ordinal ) → (a - b) o≤ a
+-→< a b = ?
+
+Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧  Injection b a → Injection (b - a) b ∧  Injection b (b - a) 
+Bernstein1 = ?
+
+Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
+Bernstein {a} {b} iab iba = be00 where
     a⊆b : * a ⊆ * b
-    a⊆b ax = subst (λ k → odef (* b) k) ? ( iB iab _ ax )
+    a⊆b {x} ax = subst (λ k → odef (* b) k) be01 ( iB iab _ ax ) where
+        be01 : i→ iab x ax ≡ x
+        be01 = ?
+        be02 : x ≡  i→ iba x ?
+        be02 = iiso iab ? ? ax ( iB iba _ ? ) ? 
     b⊆a : * b ⊆ * a
     b⊆a bx = ?
+    be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ 
+    be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥  } 
+          ind a b a<b iab iba where
+       ind :(x : Ordinal) →
+            ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
+            (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ 
+       ind x prev b x<b ixb ibx = ?
+    be00 : OrdBijection a b
+    be00 with trio< a b
+    ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
+    ... | tri≈ ¬a b ¬c = ordbij-refl b
+    ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )
 
 Card : OD
-Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
+Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
 
 record Cardinal (a : Ordinal ) : Set (suc n) where
    field
        card : Ordinal
-       ciso : Bijection a card
-       cmax : (x : Ordinal) → card o< x → ¬ Bijection a x
+       ciso : OrdBijection a card
+       cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x
 
 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
 Cardinal∈ = {!!}
--- a/src/filter.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/filter.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -12,9 +12,9 @@
 open import Data.Empty 
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
-import BAlgbra 
+import BAlgebra 
 
-open BAlgbra O
+open BAlgebra O
 
 open inOrdinal O
 open OD O
@@ -38,7 +38,7 @@
 open Bool
 
 -- Kunen p.76 and p.53, we use ⊆
-record Filter  { L P : HOD  } (LP : L ⊆ Power P) : Set (suc n) where
+record Filter { L P : HOD  } (LP : L ⊆ Power P) : Set (suc n) where
    field
        filter  : HOD   
        f⊆L     : filter ⊆ L
@@ -47,20 +47,20 @@
 
 open Filter
 
-record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
+record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter F ∋ od∅)
        prime   : {p q : HOD } → L ∋ p → L ∋ q  → L ∋ (p ∪ q) →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
 
-record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
+record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter F ∋ od∅)
        ultra   : {p : HOD } → L ∋ p → L ∋  ( P ＼ p) → ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )
 
-∈-filter : {L P p : HOD} →  {LP : L ⊆ Power P}  → (F : Filter LP ) → filter F ∋ p → L ∋ p 
+∈-filter : {L P p : HOD} →  {LP : L ⊆ Power P}  → (F : Filter {L} {P} LP ) → filter F ∋ p → L ∋ p 
 ∈-filter {L} {p} {LP} F lt = ( f⊆L F) lt 
 
-⊆-filter : {L P p q : HOD } →  {LP : L ⊆ Power P } → (F : Filter LP) →  L ∋ q → q ⊆ P
+⊆-filter : {L P p q : HOD } →  {LP : L ⊆ Power P } → (F : Filter {L} {P} LP) →  L ∋ q → q ⊆ P
 ⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( LP lt )
 
 ∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
@@ -82,7 +82,7 @@
 filter-lemma1 :  {P L : HOD} → (LP : L ⊆ Power P)
      → ({p : HOD} → L ∋ p → L ∋ (P ＼ p))
      → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))
-     → (F : Filter LP) → ultra-filter F  → prime-filter F 
+     → (F : Filter {L} {P} LP) → ultra-filter F  → prime-filter F 
 filter-lemma1 {P} {L} LP NG IN F u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
@@ -106,16 +106,16 @@
     lemma7 : filter F ∋ (q ∩ (P ＼ p))
     lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
     lemma8 : (q ∩ (P ＼ p)) ⊆ q
-    lemma8 = q∩q⊆q
+    lemma8 lt = proj1 lt
 
 -----
 --
---  if Filter contains L, prime filter is ultra
+--  if Filter {L} {P} contains L, prime filter is ultra
 --
 
 filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P)
        → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))
-       → (F : Filter LP)  → filter F ∋ P → prime-filter F → ultra-filter F
+       → (F : Filter {L} {P} LP)  → filter F ∋ P → prime-filter F → ultra-filter F
 filter-lemma2 {P} {L} LP Lm F f∋P prime = record {
          proper = prime-filter.proper prime
        ; ultra = λ {p}  L∋p _ → prime-filter.prime prime L∋p (Lm  L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L  L∋p ))  
@@ -139,7 +139,7 @@
 --  if there is a filter , there is a ultra filter under the axiom of choise
 --        Zorn Lemma
 
--- filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F : Filter LP)  → ultra-filter F
+-- filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F : Filter {L} {P} LP)  → ultra-filter F
 -- filter→ultra {P} {L} LP Lm F = {!!}
 
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
@@ -159,25 +159,25 @@
 
 open Ideal
 
-proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal LP ) → {p : HOD} → Set n
+proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n
 proper-ideal {L} {P} LP I = ideal I ∋ od∅
 
-prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal LP → ∀ {p q : HOD } → Set n
+prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n
 prime-ideal {L} {P} LP I {p} {q} =  ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q )
 
 
 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
     field
-       genf : Filter LP
-       generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
+       genf : Filter {L} {P} LP
+       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
     field
-       mf : Filter LP
+       mf : Filter {L} {P} LP
        proper  : ¬ (filter mf ∋ od∅)
-       is-maximum : ( f : Filter LP ) →  ¬ (filter f ∋ od∅)  →  ¬ filter  mf ≡ filter f → ¬ ( filter mf  ⊆ filter f  )
+       is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )
 
-max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx )
+max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx )
 max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
     mf = MaximumFilter.mf mx
     ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
@@ -185,39 +185,61 @@
     ... | yes y = case1 y
     ... | no np with ∋-p (filter mf) (P ＼ p) 
     ... | yes y = case2 y
-    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper  {!!}  ?  ) where
-         Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD
-         Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} }
+    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper  ⟪ F< , FisGreater ⟫  ) where
+         F⊆L : {y : Ordinal } → (y ≡ & p) ∨ odef (filter mf) y → odef L y
+         F⊆L (case1 refl) = lp
+         F⊆L (case2 mfx) = f⊆L mf mfx
          F : HOD
-         F = record { od = record { def = λ x → (x ≡ & p) ∨ ((y : Ordinal) → (my : odef (filter mf) y ) → x ≡ & (Y y my) )  } ; odmax = & L ; <odmax = {!!} }
-         FisFilter : Filter LP
-         FisFilter = record { filter = F ; f⊆L = {!!} ; filter1 = {!!} ; filter2 = {!!} }
-         FisGreater : {x : HOD} → filter (MaximumFilter.mf mx) ∋ x → filter FisFilter ∋ x
-         FisGreater = {!!}
+         F = record { od = record { def = λ x → (x ≡ & p) ∨ odef (filter mf) x  } ; odmax = & L ; <odmax = λ lt → odef< (F⊆L lt) } where
+         mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
+         mu01 {r} {q} Lq (case1 eq) r⊆q = mu03 where
+             r=p : r ≡ p
+             r=p = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+             mu03 : odef F (& q)
+             mu03 = ?
+         mu01 {r} {q} Lq (case2 mfr) r⊆q = case2 ( filter1 mf Lq mfr r⊆q)  
+         FisFilter : Filter {L} {P} LP
+         FisFilter = record { filter = F ; f⊆L = F⊆L ; filter1 = mu01 ; filter2 = {!!} }
+         FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
+         FisGreater {x} mfx = case2 mfx
+         F< : & (filter (MaximumFilter.mf mx)) o< & F
+         F< = ?
          FisProper : ¬ (filter FisFilter ∋ od∅)
          FisProper = {!!}
 
 open _==_
 
-open import Relation.Binary.Definitions
+-- open import Relation.Binary.Definitions
 
-ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-       → (U : Filter LP) → ultra-filter U → MaximumFilter LP 
+ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} 
+       → L ∋ p → L ∋ ( P ＼ p)) 
+       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
+       → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP 
 ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where
-  is-maximum : (F : Filter LP) → (¬ (filter F ∋ od∅)) → ( U≠F :  ¬ filter  U ≡ filter F ) →  (U⊆F : filter U  ⊆ filter F ) → ⊥
-  is-maximum F Prop U≠F U⊆F  = Prop f0 where
+  is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U  ⊂ filter F ) → ⊥
+  is-maximum F Prop ⟪ U<F , U⊆F ⟫   = Prop f0 where
      GT : HOD
-     GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = {!!} ; <odmax = {!!} }
+     GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where
+         um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L
+         um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) )
      GT≠∅ :  ¬ (GT =h= od∅)
-     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ (⊆→=  U⊆F (U-F=∅→F⊆U gt01)))) where
-         gt01 : (x : Ordinal) → ¬ odef (filter F) x ∧ (¬ odef (filter U) x)
+     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where
+         U≠F : ¬ ( filter U ≡ filter F )
+         U≠F eq = o<¬≡ (cong (&) eq) U<F
+         gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x))
          gt01 x not = ¬x<0 ( eq→ eq not )
      p : HOD
      p = ODC.minimal O GT GT≠∅
      ¬U∋p : ¬ ( filter U ∋ p )
      ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅)
+     L∋p : L ∋  p
+     L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅))
+     um00 : ¬ odef (filter U) (& p)
+     um00 = proj2 (ODC.x∋minimal O GT GT≠∅)
+     L∋-p : L ∋  ( P ＼ p )
+     L∋-p = NG L∋p
      U∋-p : filter U ∋  ( P ＼ p )
-     U∋-p with ultra-filter.ultra u {p} {!!} {!!}
+     U∋-p with ultra-filter.ultra u {p} L∋p L∋-p
      ... | case1 ux = ⊥-elim ( ¬U∋p ux )
      ... | case2 u-x = u-x
      F∋p : filter F ∋ p
@@ -225,7 +247,7 @@
      F∋-p : filter F ∋ ( P ＼ p )
      F∋-p = U⊆F U∋-p 
      f0 : filter F ∋ od∅
-     f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) )
+     f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) )
 
 import zorn 
 open zorn O _⊆_ 
@@ -240,7 +262,7 @@
 MaximumSubset {L} {P} 0<L 0<P P⊆L PO C = Zorn-lemma PO 0<P {!!}
 
 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-      → (F : Filter LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter LP 
+      → (F : Filter {L} {P} LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP 
 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
      mf01 : Maximal  {!!}  {!!}
      mf01 = MaximumSubset  0<L {!!}  {!!} {!!}  {!!}
--- a/src/generic-filter.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/generic-filter.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -15,9 +15,9 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra 
+import BAlgebra 
 
-open BAlgbra O
+open BAlgebra O
 
 open inOrdinal O
 open OD O
--- a/src/zorn.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/zorn.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -20,7 +20,7 @@
 
 open import Relation.Nullary
 open import Data.Empty
-import BAlgbra
+import BAlgebra
 
 open import Data.Nat hiding ( _<_ ; _≤_ )
 open import Data.Nat.Properties