# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1570347762 -32400
# Node ID 30e419a2be2402a78517e6a919fd489fd4197597
# Parent  7b4a66710cdd41aef8351dc1891f2631e058ad3c
disjunction and conjunction

diff -r 7b4a66710cdd -r 30e419a2be24 filter.agda
--- a/filter.agda	Mon Sep 30 21:22:07 2019 +0900
+++ b/filter.agda	Sun Oct 06 16:42:42 2019 +0900
@@ -26,11 +26,56 @@
 A ∩ B = record { def = λ x → def A x ∧ def B x } 
 
 _∪_ : ( A B : OD  ) → OD
-A ∪ B = Union (A , B)    
+A ∪ B = record { def = λ x → def A x ∨ def B x } 
+
+∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
+∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
+    lemma1 :  {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
+    lemma1 {x} lt = lemma3 lt where
+        lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
+        lemma4 {y} z with proj1 z
+        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
+        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
+        lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
+        lemma3 not = double-neg-eilm (FExists _ lemma4 not) 
+    lemma2 :  {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
+    lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
+       (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
+    lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
+       (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
+
+∩-Select : { A B : OD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
+    lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x
+    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) }
+    lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
+        record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } }
+
+dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
+dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+    lemma1 :  {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x
+    lemma1 {x} lt with proj2 lt
+    lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
+    lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
+    lemma2  : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x
+    lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } 
+    lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } 
+
+dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
+dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+    lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x
+    lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
+    lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
+    lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (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 ( record { proj1 = cq ; proj2 = cr } )
 
 record Filter  ( L : OD  ) : Set (suc n) where
    field
-       F1 : { p q : OD } → L ∋ p →  ({ x : OD} → _⊆_ q p {x} ) → L ∋ q
+       F1 : { p q : OD } → L ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → L ∋ q
        F2 : { p q : OD } → L ∋ p →  L ∋ q  → L ∋ (p ∩ q)
 
 open Filter
@@ -44,8 +89,6 @@
 ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n 
 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
 
-postulate
-   dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 
 filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
 filter-lemma1 {L} P {p} {q} u lt with u p | u q
@@ -61,10 +104,23 @@
      F1 = {!!} ; F2 = {!!}
    }
 
+record Dense  (P : OD ) : Set (suc n) where
+   field
+       dense : OD
+       incl : { x : OD} → _⊆_ dense P {x}
+       dense-f : OD → OD
+       dense-p :  { p x : OD} → P ∋ p  → _⊆_ p (dense-f p) {x} 
+
 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
 
 infinite = ZF.infinite OD→ZF
 
-Hω2 : Filter (Power (Power infinite))
-Hω2 = record { F1 = {!!} ; F2 = {!!} }
+module in-countable-ordinal {n : Level} where
+
+   import ordinal
 
+   open  ordinal.C-Ordinal-with-choice 
+
+   Hω2 : Filter (Power (Power infinite))
+   Hω2 = record { F1 = {!!} ; F2 = {!!} }
+
diff -r 7b4a66710cdd -r 30e419a2be24 ordinal.agda
--- a/ordinal.agda	Mon Sep 30 21:22:07 2019 +0900
+++ b/ordinal.agda	Sun Oct 06 16:42:42 2019 +0900
@@ -264,29 +264,30 @@
 
   _∩_ = IsZF._∩_ isZF
 
-  ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a)
-  ord-power-lemma {a} = record { eq→ = left ; eq← = right } where
-       left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x
-       left {x} lt = lemma1 where
-          lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y)))
-          lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} 
-          lemma1 : x o<  sup-o  ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) 
-          lemma1 = {!!}
-       right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x
-       right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso
-
-  uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) 
-  uncountable a y = ⊆→o<  lemma  where
-       lemma-a :  (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x}
-       lemma-a x lt = proj1 lt
-       lemma :  (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x}
-       lemma x = {!!}
-
-  continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
-  continuum-hyphotheis a x = lemma2 where
-       lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
-       lemma1 = {!!}
-       lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
-       lemma = o<→c< lemma1
-       lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
-       lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma
+-- 
+--   ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a)
+--   ord-power-lemma {a} = record { eq→ = left ; eq← = right } where
+--        left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x
+--        left {x} lt = lemma1 where
+--           lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y)))
+--           lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} 
+--           lemma1 : x o<  sup-o  ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) 
+--           lemma1 = {!!}
+--        right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x
+--        right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso
+-- 
+--   uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) 
+--   uncountable a y = ⊆→o<  lemma  where
+--        lemma-a :  (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x}
+--        lemma-a x lt = proj1 lt
+--        lemma :  (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x}
+--        lemma x = {!!}
+-- 
+--   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
+--   continuum-hyphotheis a x = lemma2 where
+--        lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
+--        lemma1 = {!!}
+--        lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
+--        lemma = o<→c< lemma1
+--        lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
+--        lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma
diff -r 7b4a66710cdd -r 30e419a2be24 zf.agda
--- a/zf.agda	Mon Sep 30 21:22:07 2019 +0900
+++ b/zf.agda	Sun Oct 06 16:42:42 2019 +0900
@@ -35,7 +35,7 @@
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
+  A ∪ B = Union (A , B)    
   ｛_｝ : ZFSet → ZFSet
   ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_