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

changeset 272:985a1af11bce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate ordered pair and Boolean Algebra
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 31 Dec 2019 11:22:52 +0900
parents 2169d948159b
children 9ccf8514c323
files BAlgbra.agda OD.agda OPair.agda cardinal.agda filter.agda
diffstat 5 files changed, 235 insertions(+), 175 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/BAlgbra.agda	Tue Dec 31 11:22:52 2019 +0900
@@ -0,0 +1,107 @@
+open import Level
+open import Ordinals
+module BAlgbra {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+import OD 
+
+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⊔_ ) 
+
+open inOrdinal O
+open OD O
+open OD.OD
+
+open _∧_
+open _∨_
+open Bool
+
+_∩_ : ( A B : OD  ) → OD
+A ∩ B = record { def = λ x → def A x ∧ def B x } 
+
+_∪_ : ( A B : OD  ) → OD
+A ∪ B = record { def = λ x → def A x ∨ def B x } 
+
+_＼_ : ( A B : OD  ) → OD
+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)   -- choice
+    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 IsBooleanAlgebra ( L : Set n)
+       ( b1 : L )
+       ( b0 : L )
+       ( -_ : L → L  )
+       ( _+_ : L → L → L )
+       ( _*_ : L → L → L ) : Set (suc n) where
+   field
+       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
+       *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
+       +-sym : {a b : L } → a + b ≡ b + a
+       -sym : {a b : L } → a * b  ≡ b * a
+       -aab : {a b : L } → a + ( a * b ) ≡ a
+       *-aab : {a b : L } → a * ( a + b ) ≡ a
+       -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
+       *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
+       a+0 : {a : L } → a + b0 ≡ a
+       a*1 : {a : L } → a * b1 ≡ a
+       a+-a1 : {a : L } → a + ( - a ) ≡ b1
+       a*-a0 : {a : L } → a * ( - a ) ≡ b0
+
+record BooleanAlgebra ( L : Set n) : Set (suc n) where
+   field
+       b1 : L
+       b0 : L
+       -_ : L → L 
+       _++_ : L → L → L
+       _**_ : L → L → L
+       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
+       
--- a/OD.agda	Mon Dec 30 23:45:59 2019 +0900
+++ b/OD.agda	Tue Dec 31 11:22:52 2019 +0900
@@ -180,106 +180,6 @@
 
 _,_ : OD  → OD  → OD 
 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
-<_,_> : (x y : OD) → OD
-< x , y > = (x , x ) , (x , y )
-
-exg-pair : { x y : OD } → (x , y ) == ( y , x )
-exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
-    left : {z : Ordinal} → def (x , y) z → def (y , x) z 
-    left (case1 t) = case2 t
-    left (case2 t) = case1 t
-    right : {z : Ordinal} → def (y , x) z → def (x , y) z 
-    right (case1 t) = case2 t
-    right (case2 t) = case1 t
-
-ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
-ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
-
-od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
-od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
-
-eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
-eq-prod refl refl = refl
-
-prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
-prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
-    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
-    lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
-    lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
-    lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
-    lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
-    lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
-    lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
-    lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
-    lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
-    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
-    lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
-        lemma3 : ( x , x ) == ( y , z )
-        lemma3 = ==-trans eq exg-pair
-    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
-    lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
-    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
-    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
-    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
-    lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
-    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
-    ... | refl with lemma2 (==-sym eq )
-    ... | refl = refl
-    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
-    lemmax : x ≡ x'
-    lemmax with eq→ eq {od→ord (x , x)} (case1 refl) 
-    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
-    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
-    ... | refl = lemma1 (ord→== s )
-    lemmay : y ≡ y'
-    lemmay with lemmax
-    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
-    ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
-
-data ord-pair : (p : Ordinal) → Set n where
-   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
-
-ZFProduct : OD
-ZFProduct = record { def = λ x → ord-pair x }
-
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
--- eq-pair refl refl = HE.refl
-
-pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi1 ( pair x y) = x
-
-π1 : { p : OD } → ZFProduct ∋ p → OD
-π1 lt = ord→od (pi1 lt )
-
-pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi2 ( pair x y ) = y
-
-π2 : { p : OD } → ZFProduct ∋ p → OD
-π2 lt = ord→od (pi2 lt )
-
-op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
-op-cons {ox} {oy} = pair ox oy
-
-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ ) 
-
-op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
-op-iso (pair ox oy) = refl
-
-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
-p-iso {x} p = ord≡→≡ (op-iso p) 
-
-p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
-p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
-
-p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
-p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
 --
 -- Axiom of choice in intutionistic logic implies the exclude middle
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/OPair.agda	Tue Dec 31 11:22:52 2019 +0900
@@ -0,0 +1,127 @@
+open import Level
+open import Ordinals
+module OPair {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+import OD 
+
+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⊔_ ) 
+
+open inOrdinal O
+open OD O
+open OD.OD
+
+open _∧_
+open _∨_
+open Bool
+
+open _==_
+
+<_,_> : (x y : OD) → OD
+< x , y > = (x , x ) , (x , y )
+
+exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
+    left : {z : Ordinal} → def (x , y) z → def (y , x) z 
+    left (case1 t) = case2 t
+    left (case2 t) = case1 t
+    right : {z : Ordinal} → def (y , x) z → def (x , y) z 
+    right (case1 t) = case2 t
+    right (case2 t) = case1 t
+
+ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
+ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
+
+od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
+
+eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod refl refl = refl
+
+prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
+    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
+    lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
+    lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
+    lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
+    lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+    lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+    lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
+    lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
+    lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
+    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
+    lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
+        lemma3 : ( x , x ) == ( y , z )
+        lemma3 = ==-trans eq exg-pair
+    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
+    lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
+    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
+    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
+    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
+    lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
+    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
+    ... | refl with lemma2 (==-sym eq )
+    ... | refl = refl
+    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
+    lemmax : x ≡ x'
+    lemmax with eq→ eq {od→ord (x , x)} (case1 refl) 
+    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
+    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
+    ... | refl = lemma1 (ord→== s )
+    lemmay : y ≡ y'
+    lemmay with lemmax
+    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
+
+data ord-pair : (p : Ordinal) → Set n where
+   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
+
+ZFProduct : OD
+ZFProduct = record { def = λ x → ord-pair x }
+
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+-- eq-pair refl refl = HE.refl
+
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y) = x
+
+π1 : { p : OD } → ZFProduct ∋ p → OD
+π1 lt = ord→od (pi1 lt )
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : OD } → ZFProduct ∋ p → OD
+π2 lt = ord→od (pi2 lt )
+
+op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
+op-cons {ox} {oy} = pair ox oy
+
+p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
+p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+    let open ≡-Reasoning in begin
+        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
+    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
+        od→ord < x , y >
+    ∎ ) 
+
+op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
+op-iso (pair ox oy) = refl
+
+p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
+p-iso {x} p = ord≡→≡ (op-iso p) 
+
+p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
+p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
+
+p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
+p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
+
--- a/cardinal.agda	Mon Dec 30 23:45:59 2019 +0900
+++ b/cardinal.agda	Tue Dec 31 11:22:52 2019 +0900
@@ -98,7 +98,7 @@
 
 open Onto
 
-onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
+onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y  → Onto X Z
 onto-restrict {X} {Y} {Z} onto  Z⊆Y = record {
      xmap = xmap1
    ; ymap = zmap
--- a/filter.agda	Mon Dec 30 23:45:59 2019 +0900
+++ b/filter.agda	Tue Dec 31 11:22:52 2019 +0900
@@ -31,80 +31,6 @@
 _＼_ : ( A B : OD  ) → OD
 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)   -- choice
-    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 IsBooleanAlgebra ( L : Set n)
-       ( b1 : L )
-       ( b0 : L )
-       ( -_ : L → L  )
-       ( _+_ : L → L → L )
-       ( _*_ : L → L → L ) : Set (suc n) where
-   field
-       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
-       *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
-       +-sym : {a b : L } → a + b ≡ b + a
-       -sym : {a b : L } → a * b  ≡ b * a
-       -aab : {a b : L } → a + ( a * b ) ≡ a
-       *-aab : {a b : L } → a * ( a + b ) ≡ a
-       -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
-       *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
-       a+0 : {a : L } → a + b0 ≡ a
-       a*1 : {a : L } → a * b1 ≡ a
-       a+-a1 : {a : L } → a + ( - a ) ≡ b1
-       a*-a0 : {a : L } → a * ( - a ) ≡ b0
-
-record BooleanAlgebra ( L : Set n) : Set (suc n) where
-   field
-       b1 : L
-       b0 : L
-       -_ : L → L 
-       _++_ : L → L → L
-       _**_ : L → L → L
-       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
-       
 
 record Filter  ( L : OD  ) : Set (suc n) where
    field