# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595635740 -32400
# Node ID 8b0715e28b33b8028c5e9283a5e99dc52bdd2b0a
# Parent  24a66a246316c2c1e5afe99e96d40a6f25cbbf2a
...

diff -r 24a66a246316 -r 8b0715e28b33 LEMC.agda
--- a/LEMC.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/LEMC.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -2,7 +2,7 @@
 open import Ordinals
 open import logic
 open import Relation.Nullary
-module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where
+module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set n) → p ∨ ( ¬ p )) where
 
 open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
@@ -23,17 +23,48 @@
 
 open import zfc
 
+open HOD
+
+open _⊆_
+
+decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
+decp  p with p∨¬p p
+decp  p | case1 x = yes x
+decp  p | case2 x = no x
+
+∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
+∋-p A x with p∨¬p ( A ∋ x)  -- LEM
+∋-p A x | case1 t  = yes t
+∋-p A x | case2 t  = no (λ x → t x)
+
+double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
+... | yes p = p
+... | no ¬p = ⊥-elim ( notnot ¬p )
+
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where
+   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
+   t1 = zf.IsZF.power→ isZF A t PA∋t
+
 --- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
-record choiced  ( X : HOD) : Set (suc n) where
+record choiced  ( X : Ordinal ) : Set n where
   field
-     a-choice : HOD
-     is-in : X ∋ a-choice
-
-open HOD
+     a-choice : Ordinal
+     is-in : odef (ord→od X) a-choice
 
 open choiced
 
+-- ∋→d : ( a : HOD  ) { x : HOD } → ord→od (od→ord a) ∋ x → X ∋ ord→od (a-choice (choice-func X not))
+-- ∋→d a lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt
+
+oo∋ : { a : HOD} {  x : Ordinal } → odef (ord→od (od→ord a)) x → a ∋ ord→od x
+oo∋ lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt
+
+∋oo : { a : HOD} {  x : Ordinal } → a ∋ ord→od x → odef (ord→od (od→ord a)) x 
+∋oo lt = subst₂ (λ j k → odef j k ) (sym oiso) diso lt 
+
 OD→ZFC : ZFC
 OD→ZFC   = record { 
     ZFSet = HOD 
@@ -47,42 +78,42 @@
     -- infixr  230 _∩_ _∪_
     isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
     isZFC = record {
-       choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
-       choice = λ A {X} A∋X not → is-in (choice-func X not)
+       choice-func = λ A {X} not A∋X → ord→od (a-choice (choice-func X not) );
+       choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not))
      } where
          --
          -- the axiom choice from LEM and OD ordering
          --
-         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (od→ord X)
          choice-func  X not = have_to_find where
-                 ψ : ( ox : Ordinal ) → Set (suc n)
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced X
+                 ψ : ( ox : Ordinal ) → Set n
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (od→ord X)
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite1 {ψ} induction ox where
-                    ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
-                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
-                    ∋-p A x | case1 (lift t)  = yes t
-                    ∋-p A x | case2 t  = no (λ x → t (lift x ))
-                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
+                 lemma-ord  ox = TransFinite {ψ} induction ox where
+                    -- ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
+                    -- ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
+                    -- ∋-p A x | case1 (lift t)  = yes t
+                    -- ∋-p A x | case2 t  = no (λ x → t (lift x ))
+                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
-                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
-                    ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
-                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
+                    ∀-imply-or  {A} {B} ∀AB | case1 t = case1 t
+                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x not )) where
                          lemma : ¬ ((x : Ordinal ) → A x) →  B
                          lemma not with p∨¬p B
                          lemma not | case1 b = b
                          lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
                     induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
                     induction x prev with ∋-p X ( ord→od x) 
-                    ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
+                    ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo  p } )
                     ... | no ¬p = lemma where
-                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X
+                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma1 y with ∋-p X (ord→od y)
-                         lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
+                         lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
                          lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma = ∀-imply-or lemma1
-                 have_to_find : choiced X
+                 have_to_find : choiced (od→ord X)
                  have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
                      ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
@@ -104,11 +135,11 @@
          open _∧_
          induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
               →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
-         induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         induction {x} prev u u∋x with p∨¬p ((y : Ordinal ) → ¬ (odef x y) ∧ (odef u y))
          ... | case1 P =
               record { min = x
-                ;     x∋min = u∋x
-                ;     min-empty = P
+                ;     x∋min = u∋x 
+                ;     min-empty = λ y → P (od→ord y)
               } 
          ... | case2 NP =  min2 where
               p : HOD
@@ -116,25 +147,25 @@
                  lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
                  lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
               np : ¬ (p =h= od∅)
-              np p∅ =  NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) 
-              y1choice : choiced p
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (subst (λ k → odef p k) (sym diso) p∋y) p∅ ) 
+              y1choice : choiced (od→ord p)
               y1choice = choice-func p np
               y1 : HOD
-              y1 = a-choice y1choice
+              y1 = ord→od (a-choice y1choice)
               y1prop : (x ∋ y1) ∧ (u ∋ y1)
-              y1prop = is-in y1choice
+              y1prop = oo∋ (is-in y1choice)
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
          Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
-         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x 
+         Min2 x u u∋x = (ε-induction {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (od→ord x )
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
-         minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
+         minimal x ne = min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
          x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
+         x∋minimal x ne = x∋min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
          minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
-         minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
+         minimal-1 x ne y = min-empty (Min2 (ord→od (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
 
 
 
diff -r 24a66a246316 -r 8b0715e28b33 OD.agda
--- a/OD.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/OD.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -76,9 +76,6 @@
 --
 --  ==→o≡ is necessary to prove axiom of extensionality.
 
-data One {n : Level } : Set n where
-  OneObj : One
-
 -- Ordinals in OD , the maximum
 Ords : OD
 Ords = record { def = λ x → One }
@@ -274,6 +271,12 @@
 open _⊆_
 infixr  220 _⊆_
 
+trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
+
+refl-⊆ : {A : HOD} → A ⊆ A
+refl-⊆ {A} = record { incl = λ x → x }
+
 od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
 od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
 
@@ -317,14 +320,14 @@
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
 -- level trick (what'a shame)
-ε-induction1 : { ψ : HOD  → Set (suc n)}
-   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : HOD ) → ψ x
-ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
-     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+-- ε-induction1 : { ψ : HOD  → Set (suc n)}
+--    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+--    → (x : HOD ) → ψ x
+-- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+--      induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+--      induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+--      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+--      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
diff -r 24a66a246316 -r 8b0715e28b33 ODC.agda
--- a/ODC.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/ODC.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -79,6 +79,13 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
+open _⊆_
+
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
+   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
+   t1 = zf.IsZF.power→ isZF A t PA∋t
+
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (od→ord y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
diff -r 24a66a246316 -r 8b0715e28b33 Ordinals.agda
--- a/Ordinals.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/Ordinals.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -24,9 +24,6 @@
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
-     TransFinite1 : { ψ : ord  → Set (suc n) }
-          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
-          →  ∀ (x : ord)  → ψ x
 
 record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
@@ -65,7 +62,6 @@
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
-        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
 
         x<nx = IsNext.x<nx (Ordinals.isNext O)
         osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
diff -r 24a66a246316 -r 8b0715e28b33 filter.agda
--- a/filter.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/filter.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -7,12 +7,9 @@
 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⊔_ ) 
 import BAlgbra 
 
 open BAlgbra O
@@ -50,17 +47,6 @@
 
 open _⊆_
 
-trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
-trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
-
-refl-⊆ : {A : HOD} → A ⊆ A
-refl-⊆ {A} = record { incl = λ x → x }
-
-power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
-power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
-   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
-   t1 = zf.IsZF.power→ isZF A t PA∋t
-
 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
 
@@ -179,447 +165,6 @@
     ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
   } where open Dense
 
--------
---    the set of finite partial functions from ω to 2
---
---
-
-data Two : Set where
-   i0 : Two
-   i1 : Two
-
-data Three : Set where
-   j0 : Three
-   j1 : Three
-   j2 : Three
-
-open import Data.List hiding (map)
-
-import OPair
-open OPair O
-
-record PFunc {n : Level} : Set (suc n) where
-   field
-      dom : Nat → Set n
-      map : (x : Nat ) → dom x → Two
-      meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q
-
-open PFunc
-
-data Findp : List Three → (x : Nat) → Set where
-   v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero
-   v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero
-   vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) 
-
-findp : List Three → (x : Nat) → Set 
-findp n x = Findp n x
-
-find : (n : List Three ) → (x : Nat) → Findp n x → Two
-find (j0 ∷ _) 0 v0 = i0
-find (j1 ∷ _) 0 v1 = i1
-find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p 
-
-Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
-Findp=n j0 n {x} {p} = refl
-Findp=n j1 n {x} {p} = refl
-Findp=n j2 n {x} {p} = refl
-
-findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
-findpeq n {0} {v0} {v0} = refl
-findpeq n {0} {v1} {v1} = refl
-findpeq [] {Suc x} {()}
-findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q})
-
-3List→PFunc : List Three → PFunc
-3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp } 
-
-_3⊆b_ : (f g : List Three) → Bool
-[] 3⊆b [] = true
-[] 3⊆b (j2 ∷ g) = [] 3⊆b g
-[] 3⊆b (_ ∷ g) = true
-(j2 ∷ f) 3⊆b [] = f 3⊆b []
-(j2 ∷ f) 3⊆b (_ ∷ g)  = f 3⊆b g
-(j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g
-(j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g
-_ 3⊆b _ = false 
-
-_3⊆_ : (f g : List Three) → Set
-f 3⊆ g  = (f 3⊆b g) ≡ true
-
-_3∩_ : (f g : List Three) → List Three
-[] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g)
-[] 3∩ g  = []
-(j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ []
-f 3∩ [] = []
-(j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g )
-(j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g )
-(_ ∷ f) 3∩ (_ ∷ g)   = j2 ∷ ( f 3∩ g )
-
-3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f
-3∩⊆f {[]} {[]} = refl
-3∩⊆f {[]} {j0 ∷ g} = refl
-3∩⊆f {[]} {j1 ∷ g} = refl
-3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g} 
-3∩⊆f {j0 ∷ f} {[]} = refl
-3∩⊆f {j1 ∷ f} {[]} = refl
-3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]}
-3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
-3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
-
-3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f )
-3∩sym {[]} {[]} = refl
-3∩sym {[]} {j0 ∷ g} = refl
-3∩sym {[]} {j1 ∷ g} = refl
-3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g})
-3∩sym {j0 ∷ f} {[]} = refl
-3∩sym {j1 ∷ f} {[]} = refl
-3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]})
-3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g})
-3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g})
-3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
-
-3⊆-[] : { h : List Three } → [] 3⊆ h
-3⊆-[] {[]} = refl
-3⊆-[] {j0 ∷ h} = refl
-3⊆-[] {j1 ∷ h} = refl
-3⊆-[] {j2 ∷ h} = 3⊆-[] {h}
-
-3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h
-3⊆trans {[]} {[]} {[]} f<g g<h = refl
-3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl
-3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl
-3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
-3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl
-3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl
-3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl
-3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl
-3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl
-3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g
-3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
-3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
-3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h 
-3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g ()
-3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g ()
-3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h
-3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g ()
-3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g ()
-3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h
-3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h 
-3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
-3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
-
-3⊆∩f : { f g h : List Three }  → f 3⊆ g → f 3⊆ h → f 3⊆  (g 3∩ h ) 
-3⊆∩f {[]} {[]} {[]} f<g f<h = refl
-3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
-3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
-3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h 
-3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g
-3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g
-3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h 
-3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h
-3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h
-3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h  
-3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
-
-3↑22 : (f : Nat → Two) (i j : Nat) → List Three
-3↑22 f Zero j = []
-3↑22 f (Suc i) j with f j
-3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
-3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)
-
-_3↑_ : (Nat → Two) → Nat → List Three
-_3↑_ f i = 3↑22 f i 0 
-
-3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x)  3⊆ (_3↑_ f y)
-3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
-     lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
-     lemma 0 y i z≤n with f i
-     lemma Zero Zero i z≤n | i0 = refl
-     lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
-     lemma Zero Zero i z≤n | i1 = refl
-     lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
-     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  
-     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y 
-     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y 
-
-Finite3b : (p : List Three ) → Bool 
-Finite3b [] = true
-Finite3b (j0 ∷ f) = Finite3b f
-Finite3b (j1 ∷ f) = Finite3b f
-Finite3b (j2 ∷ f) = false
-
-finite3cov : (p : List Three ) → List Three
-finite3cov [] = []
-finite3cov (j0 ∷ x) = j0 ∷ finite3cov x
-finite3cov (j1 ∷ x) = j1 ∷ finite3cov x
-finite3cov (j2 ∷ x) = j0 ∷ finite3cov x
-
-Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_
-Dense-3 = record {
-       dense =  λ x → Finite3b x ≡ true
-    ;  d⊆P = OneObj
-    ;  dense-f = λ x → finite3cov x
-    ;  dense-d = λ {p} d → lemma1 p
-    ;  dense-p = λ {p} d → lemma2 p
-  } where
-      lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true
-      lemma1 [] = refl
-      lemma1 (j0 ∷ p) = lemma1 p
-      lemma1 (j1 ∷ p) = lemma1 p
-      lemma1 (j2 ∷ p) = lemma1 p
-      lemma2 : (p : List Three) → p 3⊆ finite3cov p
-      lemma2 [] = refl
-      lemma2 (j0 ∷ p) = lemma2 p
-      lemma2 (j1 ∷ p) = lemma2 p
-      lemma2 (j2 ∷ p) = lemma2 p
-
-record 3Gf (f : Nat → Two) (p : List Three ) : Set where
-   field
-     3gn  : Nat
-     3f<n : p 3⊆ (f 3↑ 3gn)
-
-open 3Gf
-
-min  = Data.Nat._⊓_
--- m≤m⊔n  = Data.Nat._⊔_
-open import Data.Nat.Properties
-
-3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_
-3GF {n} f = record {  
-       filter = λ p → 3Gf f p
-     ; f⊆P = OneObj
-     ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
-     ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
- }  where
-      lemma1 : (p q : List Three ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
-      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = {!!} }
-      lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
-      lemma2 p q fp fq = {!!}
-
-record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where
-  field
-     extend : {x : Nat} → (fr : dom f x ) →  dom g x  
-     feq : {x : Nat} → {fr : dom f x } →  map f x fr ≡ map g x (extend fr)
-
-open _f⊆_
-
-_f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n}
-f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr)
-              ; map = λ x p →  map f x (proj1 p) ; meq = meq f }
-
-_↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n}
-_↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl }
-
-record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where
-   field
-     gn  : Nat
-     f<n :  (f ↑ gn) f⊆ p
-
-record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where
-   field
-     f-max :  Nat 
-     f-func :  Nat → Two
-     f-p⊆f :  p f⊆ (f-func ↑ f-max)
-     f-f⊆p :  (f-func ↑ f-max) f⊆ p 
-
-open FiniteF
-
--- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_
--- Dense-Gf = record {
---        dense =  λ x → FiniteF x
---     ;  d⊆P = lift OneObj
---     ;  dense-f = λ x → record { dom = {!!} ; map = {!!} }
---     ;  dense-d = λ {p} d → {!!}
---     ;  dense-p = λ {p} d → {!!}
---   }
-
-open Gf
-
-GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n})  ) _f⊆_ _f∩_
-GF {n} f = record {  
-       filter = λ p → Gf f p
-     ; f⊆P = lift OneObj
-     ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
-     ; filter2 = λ {p} {q} fp fq  → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
- } where
-     f1 : {p q : PFunc {n} } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
-     f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q  (extend (f<n fp )  x<g) ; feq = λ {x} {fr} → lemma {x} {fr}  } where
-         lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr))
-         lemma {x} {fr} = begin
-             map (f ↑ gn fp) x fr
-            ≡⟨ feq (f<n fp )  ⟩
-             map p x (extend (f<n fp)  fr)
-            ≡⟨ feq p⊆q  ⟩
-             map q x (extend p⊆q  (extend (f<n fp)  fr))
-            ∎  where open ≡-Reasoning 
-     f2 : {p q : PFunc {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
-     f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
-            fmin : PFunc {n}
-            fmin =  f ↑  (min (gn fp) (gn fq)) 
-            lemma1 : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr
-            lemma1 {x} x<g fr gr = begin
-                   map p x fr 
-                ≡⟨ meq p ⟩
-                   map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
-                ≡⟨ sym (feq (f<n fp)) ⟩
-                   map (f ↑  (min (gn fp) (gn fq))) x x<g
-                ≡⟨ feq (f<n fq) ⟩
-                   map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
-                ≡⟨ meq q ⟩
-                   map q x gr
-                ∎  where open ≡-Reasoning 
-            lemma2  : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x
-            lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ;
-                     proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }}
-            f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q
-            f∩→⊆ p q = record {
-                   extend = λ {x} pq → proj1 (proj2 pq)
-                 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) 
-                }
-            lemma3 :  {x : Nat}  → ( fr : Lift n (x ≤ min (gn fp) (gn fq)))  → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr)
-            lemma3 {x} fr = 
-                  map (f ↑ min (gn fp) (gn fq)) x fr
-                ≡⟨ feq (f<n fq) ⟩
-                  map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
-                ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} )   ⟩
-                  map (p f∩ q) x (lemma2 fr)
-                ∎  where open ≡-Reasoning 
-
-
-ODSuc : (y : HOD) → infinite ∋ y → HOD
-ODSuc y lt = Union (y , (y , y)) 
-
-data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
-  hφ :  Hω2 0 o∅
-  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) ,  ord→od x )))
-  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) ,  ord→od x )))
-  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) x
-
-record  Hω2r (x : Ordinal) : Set n where
-  field
-    count : Nat
-    hω2 : Hω2 count x
-
-open Hω2r
-
-HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
-    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
-    ω<next = ω<next-o∅ ho<
-    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
-    lemma = {!!}
-    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
-    odmax0 {y} r with hω2 r
-    ... | hφ = x<nx
-    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
-    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
-    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
-
-3→Hω2 : List Three → HOD
-3→Hω2 t = list→hod t 0 where
-   list→hod : List Three → Nat → HOD
-   list→hod [] _ = od∅
-   list→hod (j0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
-   list→hod (j1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
-   list→hod (j2 ∷ t) i = list→hod t (Suc i ) 
-
-Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Three 
-Hω2→3 x = lemma where
-   lemma : { y : Ordinal } →  Hω2r y → List Three
-   lemma record { count = 0 ; hω2 = hφ } = []
-   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = j0 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = j1 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (he hω3) } = j2 ∷ lemma record { count = i ; hω2 =  hω3 }
-
-ω→2 : HOD
-ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ x → < x , repl p x > )) where
-  repl : HOD → HOD → HOD
-  repl p x with ODC.∋-p O p x
-  ... | yes _  = nat→ω 1
-  ... | no _  = nat→ω 0
-
-ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
-ω→2f x = {!!}
-
-↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
-↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
-
-record Gfo (x : Ordinal) : Set n where
-  field
-     gfunc : Ordinal
-     gmax : Ordinal
-     gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
-     gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x 
-     pcond : odef HODω2 x
-
-open Gfo
-
-HODGf : HOD
-HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }
-
-G : (Nat → Two) → Filter HODω2
-G f = record {
-       filter = HODGf
-     ; f⊆PL = {!!}
-     ; filter1 = {!!}
-     ; filter2 = {!!}
-   } where
-       filter0 : HOD   
-       filter0 = {!!}
-       f⊆PL1 :  filter0 ⊆ Power HODω2 
-       f⊆PL1 = {!!}
-       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
-       filter11 = {!!}
-       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
-       filter12 = {!!}
-
--- the set of finite partial functions from ω to 2
-
-Hω2f : Set (suc n)
-Hω2f = (Nat → Set n) → Two
-
-Hω2f→Hω2 : Hω2f  → HOD
-Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
-
-
-record CountableOrdinal : Set (suc (suc n)) where
-   field
-       ctl→ : Nat → Ordinal
-       ctl← : Ordinal → Nat
-       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
-       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
        
 record GenericFilter (P : HOD) : Set (suc n) where
     field
@@ -632,12 +177,3 @@
        Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
        Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )
 
-data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (n : Nat) →  Set (suc n) where
-    pd0 : (p : Ordinal ) → odef (ord→od P) p → PD C p 0 
-    pdq : {q pnx : Ordinal } {n : Nat}  → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) 
-
-P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P
-P-GenericFilter {P} C = record {
-      genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
-    ; generic = λ D → {!!}
-   }
diff -r 24a66a246316 -r 8b0715e28b33 generic-filter.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/generic-filter.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -0,0 +1,269 @@
+open import Level
+open import Ordinals
+module generic-filter {n : Level } (O : Ordinals {n})   where
+
+import filter 
+open import zf
+open import logic
+open import partfunc {n} O
+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⊔_ ) 
+import BAlgbra 
+
+open BAlgbra O
+
+open inOrdinal O
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+
+import ODC
+
+open filter O
+
+open _∧_
+open _∨_
+open Bool
+
+
+open HOD
+
+-------
+--    the set of finite partial functions from ω to 2
+--
+--
+
+open import Data.List 
+open import Data.Maybe 
+
+import OPair
+open OPair O
+
+open PFunc
+
+_f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) →  PFunc (Lift n Nat) (Lift n Two)
+f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → pmap f x fr ≡ pmap g x gr)
+              ; pmap = λ x p →  pmap f x (proj1  p) ; meq = meq f }
+
+_↑_ :  (Nat → Two) → Nat →  PFunc (Lift n Nat) (Lift n Two)
+_↑_  f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl }
+
+record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two)  ) : Set (suc n) where
+  field
+     extend : {x : Nat} → (fr : dom f (lift x) ) →  dom g (lift x  )
+     feq : {x : Nat} → {fr : dom f (lift x) } →  pmap f (lift x) fr ≡ pmap g (lift x) (extend fr)
+
+record Gf (f : Nat → Two) (p :  PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where
+   field
+     gn  : Nat
+     f<n :  (f ↑ gn) f⊆ p
+
+record FiniteF (p :  PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where
+   field
+     f-max :  Nat 
+     f-func :  Nat → Two
+     f-p⊆f :  p f⊆ (f-func ↑ f-max)
+     f-f⊆p :  (f-func ↑ f-max) f⊆ p 
+
+open FiniteF
+
+
+-- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_
+-- Dense-Gf = record {
+--        dense =  λ x → FiniteF x
+--     ;  d⊆P = lift OneObj
+--     ;  dense-f = λ x → record { dom = {!!} ; pmap = {!!} }
+--     ;  dense-d = λ {p} d → {!!}
+--     ;  dense-p = λ {p} d → {!!}
+--   }
+
+open Gf
+open _f⊆_ 
+open import Data.Nat.Properties
+
+GF :  (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n})  ) _f⊆_ _f∩_
+GF  f = record {  
+       filter = λ p → Gf f p
+     ; f⊆P = lift OneObj
+     ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
+     ; filter2 = λ {p} {q} fp fq  → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
+ } where
+     f1 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
+     f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q  (extend (f<n fp )  x<g) ; feq = λ {x} {fr} → lemma {x} {fr}  } where
+         lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr))
+         lemma {x} {fr} = begin
+             pmap (f ↑ gn fp) (lift x) fr
+            ≡⟨ feq (f<n fp )  ⟩
+             pmap p (lift x) (extend (f<n fp)  fr)
+            ≡⟨ feq p⊆q  ⟩
+             pmap q (lift x) (extend p⊆q  (extend (f<n fp)  fr))
+            ∎  where open ≡-Reasoning 
+     f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf  f p ) → (fq : Gf  f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
+     f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
+            fmin : PFunc (Lift n Nat) (Lift n Two)
+            fmin =  f ↑  (min (gn fp) (gn fq)) 
+            lemma1 : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr
+            lemma1 {x} x<g fr gr = begin
+                   pmap p (lift x) fr 
+                ≡⟨ meq p ⟩
+                   pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
+                ≡⟨ sym (feq (f<n fp)) ⟩
+                   pmap (f ↑  (min (gn fp) (gn fq))) (lift x) x<g
+                ≡⟨ feq (f<n fq) ⟩
+                   pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
+                ≡⟨ meq q ⟩
+                   pmap q (lift x) gr
+                ∎  where open ≡-Reasoning 
+            lemma2  : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift x)
+            lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ;
+                     proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }}
+            f∩→⊆ : (p q : PFunc (Lift n Nat) (Lift n Two) ) → (p f∩ q ) f⊆ q
+            f∩→⊆ p q = record {
+                   extend = λ {x} pq → proj1 (proj2 pq)
+                 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) 
+                }
+            lemma3 :  {x : Nat}  → ( fr : Lift n (x ≤ min (gn fp) (gn fq)))  → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr)
+            lemma3 {x} fr = 
+                  pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr
+                ≡⟨ feq (f<n fq) ⟩
+                  pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
+                ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} )   ⟩
+                  pmap (p f∩ q) (lift x) (lemma2 fr)
+                ∎  where open ≡-Reasoning 
+
+
+ODSuc : (y : HOD) → infinite ∋ y → HOD
+ODSuc y lt = Union (y , (y , y)) 
+
+data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
+  hφ :  Hω2 0 o∅
+  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) ,  ord→od x )))
+  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) ,  ord→od x )))
+  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
+    Hω2 (Suc i) x
+
+record  Hω2r (x : Ordinal) : Set n where
+  field
+    count : Nat
+    hω2 : Hω2 count x
+
+open Hω2r
+
+HODω2 :  HOD
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
+    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
+    ω<next = ω<next-o∅ ho<
+    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
+    lemma = {!!}
+    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
+    odmax0 {y} r with hω2 r
+    ... | hφ = x<nx
+    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
+    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
+    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
+
+3→Hω2 : List (Maybe Two) → HOD
+3→Hω2 t = list→hod t 0 where
+   list→hod : List (Maybe Two) → Nat → HOD
+   list→hod [] _ = od∅
+   list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
+   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
+   list→hod (nothing ∷ t) i = list→hod t (Suc i ) 
+
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
+Hω2→3 x = lemma where
+   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
+   lemma record { count = 0 ; hω2 = hφ } = []
+   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
+
+ω→2 : HOD
+ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ x → < x , repl p x > )) where
+  repl : HOD → HOD → HOD
+  repl p x with ODC.∋-p O p x
+  ... | yes _  = nat→ω 1
+  ... | no _  = nat→ω 0
+
+ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
+ω→2f x = {!!}
+
+↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
+↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
+
+record Gfo (x : Ordinal) : Set n where
+  field
+     gfunc : Ordinal
+     gmax : Ordinal
+     gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
+     gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x 
+     pcond : odef HODω2 x
+
+open Gfo
+
+HODGf : HOD
+HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }
+
+G : (Nat → Two) → Filter HODω2
+G f = record {
+       filter = HODGf
+     ; f⊆PL = {!!}
+     ; filter1 = {!!}
+     ; filter2 = {!!}
+   } where
+       filter0 : HOD   
+       filter0 = {!!}
+       f⊆PL1 :  filter0 ⊆ Power HODω2 
+       f⊆PL1 = {!!}
+       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
+       filter11 = {!!}
+       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
+       filter12 = {!!}
+
+-- the set of finite partial functions from ω to 2
+
+Hω2f : Set (suc n)
+Hω2f = (Nat → Set n) → Two
+
+Hω2f→Hω2 : Hω2f  → HOD
+Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
+
+
+record CountableOrdinal : Set (suc (suc n)) where
+   field
+       ctl→ : Nat → Ordinal
+       ctl← : Ordinal → Nat
+       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
+       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
+       
+open CountableOrdinal 
+
+PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n
+PGOD  i C p q =  ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x →  odef (ord→od q) x ))
+
+PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
+PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } 
+
+ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal
+ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q )
+ord-compare i C p q | case1 y = p
+ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) 
+
+data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set (suc n) where
+    pd0 : PD P C o∅ 0 
+    -- pdq : {q pnx : Ordinal } {n : Nat}  → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) 
+
+P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P
+P-GenericFilter {P} C = record {
+      genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+    ; generic = λ D → {!!}
+   }
diff -r 24a66a246316 -r 8b0715e28b33 logic.agda
--- a/logic.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/logic.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -5,6 +5,12 @@
 open import Relation.Binary
 open import Data.Empty
 
+data One {n : Level } : Set n where
+  OneObj : One
+
+data Two : Set where
+   i0 : Two
+   i1 : Two
 
 data Bool : Set where
    true : Bool
diff -r 24a66a246316 -r 8b0715e28b33 partfunc.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/partfunc.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -0,0 +1,233 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Level
+open import Relation.Nullary 
+open import Relation.Binary.PropositionalEquality
+open import Ordinals
+module partfunc {n : Level } (O : Ordinals {n})  where
+
+open import logic
+open import Relation.Binary 
+open import Data.Empty 
+open import Data.List 
+open import Data.Maybe  
+open import Relation.Binary
+open import Relation.Binary.Core
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import filter O
+
+open _∧_
+open _∨_
+open Bool
+
+
+record PFunc  (Dom : Set n) (Cod : Set n) : Set (suc n) where
+   field
+      dom : Dom → Set n
+      pmap : (x : Dom ) → dom x → Cod
+      meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
+
+
+data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where
+   v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v  ∷ f ) Zero
+   vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) 
+
+open PFunc
+
+find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
+find (just v ∷ _) 0 (v0 v) = v
+find (_ ∷ n) (Suc i) (vn p) = find n i p
+
+findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
+findpeq n {0} {v0 _} {v0 _} = refl
+findpeq [] {Suc x} {()}
+findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
+findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
+
+List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
+List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x))
+                       ; pmap = λ x y → find fp (lower x) (lower y)
+                       ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} 
+                       }
+
+_3⊆b_ : (f g : List (Maybe Two)) → Bool
+[] 3⊆b [] = true
+[] 3⊆b (nothing ∷ g) = [] 3⊆b g
+[] 3⊆b (_ ∷ g) = true
+(nothing ∷ f) 3⊆b [] = f 3⊆b []
+(nothing ∷ f) 3⊆b (_ ∷ g)  = f 3⊆b g
+(just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g
+(just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g
+_ 3⊆b _ = false 
+
+_3⊆_ : (f g : List (Maybe Two)) → Set
+f 3⊆ g  = (f 3⊆b g) ≡ true
+
+_3∩_ : (f g : List (Maybe Two)) → List (Maybe Two)
+[] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g)
+[] 3∩ g  = []
+(nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ []
+f 3∩ [] = []
+(just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ (  f 3∩ g )
+(just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ (  f 3∩ g )
+(_ ∷ f) 3∩ (_ ∷ g)   = nothing  ∷ ( f 3∩ g )
+
+3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f
+3∩⊆f {[]} {[]} = refl
+3∩⊆f {[]} {just _ ∷ g} = refl
+3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g} 
+3∩⊆f {just _ ∷ f} {[]} = refl
+3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]}
+3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {just i1 ∷ f} {just i1 ∷ g} =  3∩⊆f {f} {g}
+3∩⊆f {just i0 ∷ f} {just i1 ∷ g} =   3∩⊆f {f} {g}
+3∩⊆f {just i1 ∷ f} {just i0 ∷ g} =    3∩⊆f {f} {g}
+3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {just i0  ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g} 
+3∩⊆f {just i1 ∷ f} {nothing ∷ g} =  3∩⊆f {f} {g} 
+3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
+
+3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f )
+3∩sym {[]} {[]} = refl
+3∩sym {[]} {just _ ∷ g} = refl
+3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g})
+3∩sym {just _ ∷ f} {[]} = refl
+3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]})
+3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g})
+3∩sym {just i0 ∷ f} {just i1 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {just i1 ∷ f} {just i0 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {just i1 ∷ f} {just i1 ∷ g} =  cong (λ k → just i1 ∷ k) (3∩sym {f} {g})
+3∩sym {just i0 ∷ f} {nothing ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {just i1 ∷ f} {nothing ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {nothing ∷ f} {just i1 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
+
+3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h
+3⊆-[] {[]} = refl
+3⊆-[] {just _ ∷ h} = refl
+3⊆-[] {nothing ∷ h} = 3⊆-[] {h}
+
+3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h
+3⊆trans {[]} {[]} {[]} f<g g<h = refl
+3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl
+3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
+3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl
+3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl
+3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl
+3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h 
+3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g
+3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
+3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h 
+3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h 
+3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {[]} {just i0 ∷ g} {[]} f<g ()
+3⊆trans {[]} {just i1 ∷ g} {[]} f<g ()
+3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h}
+3⊆trans {just i0 ∷ f} {[]} {h} () g<h
+3⊆trans {just i1 ∷ f} {[]} {h} () g<h
+3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g ()
+3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g ()
+3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
+3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
+3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
+3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
+3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h
+3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h
+3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g ()
+3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g ()
+3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
+3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
+3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
+3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
+
+3⊆∩f : { f g h : List (Maybe Two) }  → f 3⊆ g → f 3⊆ h → f 3⊆  (g 3∩ h ) 
+3⊆∩f {[]} {[]} {[]} f<g f<h = refl
+3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
+3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
+3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h 
+3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g
+3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h 
+3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h
+3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h =   3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h =   3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h  
+3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+
+3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two)
+3↑22 f Zero j = []
+3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j)
+
+_3↑_ : (Nat → Two) → Nat → List (Maybe Two)
+_3↑_ f i = 3↑22 f i 0 
+
+3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x)  3⊆ (_3↑_ f y)
+3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
+     lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
+     lemma 0 y i z≤n with f i
+     lemma Zero Zero i z≤n | i0 = refl
+     lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
+     lemma Zero Zero i z≤n | i1 = refl
+     lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
+     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y 
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y 
+
+Finite3b : (p : List (Maybe Two) ) → Bool 
+Finite3b [] = true
+Finite3b (just _ ∷ f) = Finite3b f
+Finite3b (nothing ∷ f) = false
+
+finite3cov : (p : List (Maybe Two) ) → List (Maybe Two)
+finite3cov [] = []
+finite3cov (just y ∷ x) = just y ∷ finite3cov x
+finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x
+
+Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
+Dense-3 = record {
+       dense =  λ x → Finite3b x ≡ true
+    ;  d⊆P = OneObj
+    ;  dense-f = λ x → finite3cov x
+    ;  dense-d = λ {p} d → lemma1 p
+    ;  dense-p = λ {p} d → lemma2 p
+  } where
+      lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true
+      lemma1 [] = refl
+      lemma1 (just i0 ∷ p) = lemma1 p
+      lemma1 (just i1 ∷ p) = lemma1 p
+      lemma1 (nothing ∷ p) = lemma1 p
+      lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p
+      lemma2 [] = refl
+      lemma2 (just i0 ∷ p) = lemma2 p
+      lemma2 (just i1 ∷ p) = lemma2 p
+      lemma2 (nothing ∷ p) = lemma2 p
+
+record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where
+   field
+     3gn  : Nat
+     3f<n : p 3⊆ (f 3↑ 3gn)
+
+open 3Gf
+
+min  = Data.Nat._⊓_
+-- m≤m⊔n  = Data.Nat._⊔_
+open import Data.Nat.Properties
+
+3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_
+3GF {n} f = record {  
+       filter = λ p → 3Gf f p
+     ; f⊆P = OneObj
+     ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
+     ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
+ }  where
+      lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
+      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = {!!} }
+      lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
+      lemma2 p q fp fq = ?