# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596272723 -32400
# Node ID 9984cdd88da335dbfad5cdeb3f6e474cdcdc7174
# Parent  44a484f17f26a6ad382cb6c51fe20ca98665ae2a
...

diff -r 44a484f17f26 -r 9984cdd88da3 BAlgbra.agda
--- a/BAlgbra.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/BAlgbra.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -94,9 +94,9 @@
        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
+       +-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 )
+       +-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
diff -r 44a484f17f26 -r 9984cdd88da3 OD.agda
--- a/OD.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/OD.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -34,11 +34,8 @@
      eq→ : ∀ { x : Ordinal  } → def a x → def b x 
      eq← : ∀ { x : Ordinal  } → def b x → def a x 
 
-id : {A : Set n} → A → A
-id x = x
-
 ==-refl :  {  x :  OD  } → x == x
-==-refl  {x} = record { eq→ = id ; eq← = id }
+==-refl  {x} = record { eq→ = λ x → x ; eq← = λ x → x }
 
 open  _==_ 
 
@@ -148,23 +145,12 @@
 d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (* x)
 d→∋ a lt = subst (λ k → odef a k ) (sym &iso) lt
 
-cseq :  HOD  →  HOD 
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
-    lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
-    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) 
-
-odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
-odef-subst df refl refl = df
+-- odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
+-- odef-subst df refl refl = df
 
 otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
-odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X 
-odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( odef-subst  {X} {x}  lt (sym *iso) (sym &iso) )) &iso &iso
-
-odefo→o< :  {X y : Ordinal } → odef (* X) y → y o< X
-odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) &iso &iso ( c<→o< (subst (λ k → odef (* X) k ) (sym &iso ) lt ))
-
 -- If we have reverse of c<→o<, everything becomes Ordinal
 o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (* y) x ) → {x : HOD } →  x ≡ Ord (& x)
 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
@@ -179,11 +165,11 @@
 
 ==-iso : { x y : HOD  } → od (* (& x)) == od (* (& y))  →  od x == od y
 ==-iso  {x} {y} eq = record {
-      eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym *iso) refl )) ;
-      eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym *iso) refl ))  }
+      eq→ = λ {z} d →  lemma ( eq→  eq (subst (λ k → odef k z ) (sym *iso) d )) ; 
+      eq← = λ {z} d →  lemma ( eq←  eq (subst (λ k → odef k z ) (sym *iso) d )) } 
         where
            lemma : {x : HOD  } {z : Ordinal } → odef (* (& x)) z → odef x z
-           lemma {x} {z} d = odef-subst d *iso refl
+           lemma {x} {z} d = subst (λ k → odef k z) (*iso) d 
 
 =-iso :  {x y : HOD  } → (od x == od y) ≡ (od (* (& x)) == od y)
 =-iso  {_} {y} = cong ( λ k → od k == od y ) (sym *iso)
@@ -199,7 +185,8 @@
 o∅≡od∅ : * (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
      lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x
-     lemma0 {x} lt = o<-subst (c<→o<  {* x} {* o∅} (odef-subst  {* o∅} {x} lt refl (sym &iso)) ) &iso &iso
+     lemma0 {x} lt with c<→o< {* x} {* o∅} (subst (λ k → odef (* o∅) k ) (sym &iso) lt)
+     ... | t = subst₂ (λ j k → j o< k ) &iso &iso t
      lemma1 :  {x : Ordinal} → odef od∅ x → odef (* o∅) x
      lemma1 {x} lt = ⊥-elim (¬x<0 lt)
      lemma : od (* o∅) == od od∅
@@ -235,27 +222,6 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
-pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
-pair-xx<xy {x} {y} = ⊆→o≤  lemma where
-   lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
-   lemma {z} (case1 refl) = case1 refl
-   lemma {z} (case2 refl) = case1 refl
-
-pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
-... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< 
-... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< 
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< 
-
---  another form of infinite
--- pair-ord< :  {x : Ordinal } → Set n
-pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
-pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
-       lemmab0 : next (odmax (x , x)) ≡ next (& x)
-       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
-       lemmab1 : & (x , x) o< next ( odmax (x , x))
-       lemmab1 = ho<
-
 pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
    lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
@@ -280,15 +246,6 @@
 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 → & x o< osuc (& y)
-od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
-
 -- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
 ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
    →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
@@ -306,19 +263,6 @@
     lemma1 : osuc (& y) o< & (x , x)
     lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) 
 
-subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
-subset-lemma  {A} {x} = record {
-      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
-    ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
-   } 
-
-power< : {A x : HOD  } → x ⊆ A → Ord (osuc (& A)) ∋ x
-power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) &iso (lemma y x∋y ) ) where
-    lemma : (y : Ordinal) → def (od x) y → def (od A) (& (* y))
-    lemma y x∋y = incl x⊆A (d→∋ x x∋y)
-
-open import Data.Unit
-
 ε-induction : { ψ : HOD  → Set n}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
@@ -415,9 +359,6 @@
 -- infinite : HOD 
 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
-odsuc : (y : HOD) → HOD
-odsuc y = Union (y , (y , y))
-
 infinite : HOD 
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
     u : (y : Ordinal ) → HOD
@@ -441,32 +382,12 @@
     lemma {o∅} iφ = x<nx
     lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
 
-ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
-ω<next-o∅ {y} lt = <odmax infinite lt
-
-nat→ω : Nat → HOD
-nat→ω Zero = od∅
-nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
-
-ω→nato : {y : Ordinal} → infinite-d y → Nat
-ω→nato iφ = Zero
-ω→nato (isuc lt) = Suc (ω→nato lt)
-
-ω→nat : (n : HOD) → infinite ∋ n → Nat
-ω→nat n = ω→nato 
-
-ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
-ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
-ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
-    lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
-    lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
+empty : (x : HOD  ) → ¬  (od∅ ∋ x)
+empty x = ¬x<0 
 
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
 
-infixr  200 _∈_
--- infixr  230 _∩_ _∪_
-
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y ) 
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))
 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y ))
@@ -475,19 +396,6 @@
 pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) (==→o≡ t=h=x))
 pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y))
 
-pair1 : { x y  : HOD  } →  (x , y ) ∋ x
-pair1 = case1 refl
-
-pair2 : { x y  : HOD  } →  (x , y ) ∋ y
-pair2 = case2 refl
-
-single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
-single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
-single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
-
-empty : (x : HOD  ) → ¬  (od∅ ∋ x)
-empty x = ¬x<0 
-
 o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) 
 o<→c< lt = record { incl = λ z → ordtrans z lt }  
 
@@ -498,80 +406,6 @@
 ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
-
-ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
-ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y))
-      ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where
-   lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y))
-   lemma u t with proj1 t
-   lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
-        (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u)
-   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso )  (proj2 t))) x<y where
-       lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y    --  y = x ∈ ( x , x ) = u 
-       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
-       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
-
-ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
-ω-prev-eq {x} {y} eq with trio< x y
-ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
-ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
-ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
-
-ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
-ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫
-
-ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
-ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
-
-nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
-nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
-     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
-                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
-     ind {x} prev lt = ind1 lt *iso where
-         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
-         ind1 {o∅} iφ refl = sym o∅≡od∅
-         ind1 (isuc {x₁} ltd) ox=x = begin
-              nat→ω (ω→nato (isuc ltd) )         
-           ≡⟨⟩
-              Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
-           ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
-              Union (* x₁ , (* x₁ , * x₁))
-           ≡⟨ trans ( sym *iso) ox=x ⟩
-              x 
-           ∎ where
-               open ≡-Reasoning 
-               lemma0 :  x ∋ * x₁
-               lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not 
-                  (& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
-               lemma1 : infinite ∋ * x₁
-               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
-               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
-               lemma3 iφ iφ refl = HE.refl
-               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
-               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
-               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
-               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
-               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
-               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
-                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
-                   lemma6 refl HE.refl = refl
-               lemma :  nat→ω (ω→nato ltd) ≡ * x₁
-               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
-
-ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
-   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
-   lemma {x} Zero iφ eq = refl
-   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
-   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
-   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
-           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
-           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
-                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
-                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
-
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
@@ -588,12 +422,12 @@
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
 replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where 
     lemma : def (in-codomain X ψ) (& (ψ x))
-    lemma not = ⊥-elim ( not ( & x ) (⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ ))
+    lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
     lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y))))
             → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)))
-    lemma2 not not2  = not ( λ y d →  not2 y (⟪ proj1 d , lemma3 (proj2 d)⟫)) where
+    lemma2 not not2  = not ( λ y d →  not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where
         lemma3 : {y : Ordinal } → (& x ≡ & (ψ (*  y))) → (* (& x) =h= ψ (* y))  
         lemma3 {y} eq = subst (λ k  → * (& x) =h= k ) *iso (o≡→== eq )
     lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) )
@@ -609,7 +443,7 @@
 --
 ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
 ∩-≡ {a} {b} inc = record {
-   eq→ = λ {x} x<a → ⟪ odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl &iso , x<a  ⟫ ;
+   eq→ = λ {x} x<a → ⟪ (subst (λ k → odef b k ) &iso (inc (d→∋ a x<a))) , x<a  ⟫ ;
    eq← = λ {x} x<a∩b → proj2 x<a∩b }
 -- 
 -- Transitive Set case
@@ -618,11 +452,10 @@
 -- OPwr  A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) )   
 -- 
 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
-ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {& t}
-        lemma refl (lemma1 lemma-eq )where
+ord-power← a t t→A  = subst (λ k → odef (OPwr (Ord a)) k ) (lemma1 lemma-eq) lemma where 
     lemma-eq :  ((Ord a) ∩ t) =h= t
     eq→ lemma-eq {z} w = proj2 w 
-    eq← lemma-eq {z} w = ⟪ odef-subst  {_} {_} {(Ord a)} {z} ( t→A (d→∋ t w)) refl &iso  , w ⟫
+    eq← lemma-eq {z} w = ⟪ subst (λ k → odef (Ord a) k ) &iso ( t→A (d→∋ t w)) , w ⟫ 
     lemma1 :  {a : Ordinal } { t : HOD }
         → (eq : ((Ord a) ∩ t) =h= t)  → & ((Ord a) ∩ (* (& t))) ≡ & t
     lemma1  {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq ))
@@ -718,21 +551,11 @@
     lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
         lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 )
     lemma2 :  def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t)
-    lemma2 not = ⊥-elim ( not (& t) (⟪ lemma3 , lemma6 ⟫) ) where
+    lemma2 not = ⊥-elim ( not (& t) ⟪ lemma3 , lemma6 ⟫ ) where
         lemma6 : & t ≡ & (A ∩ * (& t)) 
         lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A  )))
 
 
-ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
-ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
-    lemma : {x y : HOD} → & x o< osuc a → x ∋ y →  Ord a ∋ y
-    lemma lt y<x with osuc-≡< lt
-    lemma lt y<x | case1 refl = c<→o< y<x
-    lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
-
-continuum-hyphotheis : (a : Ordinal) → Set (suc n)
-continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
-
 extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym &iso) (proj1 (eq (* x))) d  
 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym &iso) (proj2 (eq (* x))) d  
@@ -742,7 +565,7 @@
 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
 infinity∅ : infinite  ∋ od∅ 
-infinity∅ = odef-subst  {_} {_} {infinite} {& (od∅ )} iφ refl lemma where
+infinity∅ = subst (λ k → odef infinite k ) lemma iφ where 
     lemma : o∅ ≡ & od∅
     lemma =  let open ≡-Reasoning in begin
         o∅
@@ -752,7 +575,7 @@
         & od∅
         ∎
 infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-infinity x lt = odef-subst  {_} {_} {infinite} {& (Union (x , (x , x )))} ( isuc {& x} lt ) refl lemma where
+infinity x lt = subst (λ k → odef infinite k ) lemma (isuc {& x} lt) where
     lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
         ≡ & (Union (x , (x , x)))
     lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso 
@@ -774,8 +597,6 @@
     ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
     ;   replacement← = replacement←
     ;   replacement→ = λ {ψ} → replacement→ {ψ}
-    -- ;   choice-func = choice-func
-    -- ;   choice = choice
     } 
 
 HOD→ZF : ZF  
diff -r 44a484f17f26 -r 9984cdd88da3 ODUtil.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ODUtil.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -0,0 +1,177 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+open import Level
+open import Ordinals
+module ODUtil {n : Level } (O : Ordinals {n} ) where
+
+open import zf
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.Core
+
+open import logic
+open import nat
+
+open inOrdinal O
+open import nat
+
+import OD
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+
+open HOD
+open _⊆_
+open _∧_
+open _==_
+
+cseq :  HOD  →  HOD 
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
+    lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
+    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) 
+
+
+pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
+pair-xx<xy {x} {y} = ⊆→o≤  lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
+   lemma {z} (case1 refl) = case1 refl
+   lemma {z} (case2 refl) = case1 refl
+
+pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
+pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
+... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< 
+... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< 
+... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< 
+
+--  another form of infinite
+-- pair-ord< :  {x : Ordinal } → Set n
+pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
+pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
+       lemmab0 : next (odmax (x , x)) ≡ next (& x)
+       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
+       lemmab1 : & (x , x) o< next ( odmax (x , x))
+       lemmab1 = ho<
+
+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 → & x o< osuc (& y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
+
+subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma  {A} {x} = record {
+      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
+    ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
+   } 
+
+
+ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+ω<next-o∅ {y} lt = <odmax infinite lt
+
+nat→ω : Nat → HOD
+nat→ω Zero = od∅
+nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+
+ω→nato : {y : Ordinal} → infinite-d y → Nat
+ω→nato iφ = Zero
+ω→nato (isuc lt) = Suc (ω→nato lt)
+
+ω→nat : (n : HOD) → infinite ∋ n → Nat
+ω→nat n = ω→nato 
+
+ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
+ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
+ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
+    lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
+    lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
+
+pair1 : { x y  : HOD  } →  (x , y ) ∋ x
+pair1 = case1 refl
+
+pair2 : { x y  : HOD  } →  (x , y ) ∋ y
+pair2 = case2 refl
+
+single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
+single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
+single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
+
+ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
+ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y))
+      ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where
+   lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y))
+   lemma u t with proj1 t
+   lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
+        (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u)
+   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso )  (proj2 t))) x<y where
+       lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y    --  y = x ∈ ( x , x ) = u 
+       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
+       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
+
+ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
+ω-prev-eq {x} {y} eq with trio< x y
+ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
+ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
+ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
+
+ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
+ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫
+
+ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
+ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
+
+nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
+     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
+                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
+     ind {x} prev lt = ind1 lt *iso where
+         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
+         ind1 {o∅} iφ refl = sym o∅≡od∅
+         ind1 (isuc {x₁} ltd) ox=x = begin
+              nat→ω (ω→nato (isuc ltd) )         
+           ≡⟨⟩
+              Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
+           ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
+              Union (* x₁ , (* x₁ , * x₁))
+           ≡⟨ trans ( sym *iso) ox=x ⟩
+              x 
+           ∎ where
+               open ≡-Reasoning 
+               lemma0 :  x ∋ * x₁
+               lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not 
+                  (& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
+               lemma1 : infinite ∋ * x₁
+               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
+               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
+               lemma3 iφ iφ refl = HE.refl
+               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
+               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
+               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
+               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
+               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
+               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
+                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
+                   lemma6 refl HE.refl = refl
+               lemma :  nat→ω (ω→nato ltd) ≡ * x₁
+               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
+
+ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
+ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
+   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
+   lemma {x} Zero iφ eq = refl
+   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
+   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
+   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
+           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
+           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
+                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
+                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
+
diff -r 44a484f17f26 -r 9984cdd88da3 OrdUtil.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/OrdUtil.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -0,0 +1,287 @@
+open import Level
+open import Ordinals
+module OrdUtil {n : Level} (O : Ordinals {n} ) where
+
+open import logic
+open import nat
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import Relation.Binary
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal 
+open Ordinals.IsNext isNext 
+
+o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
+o<-dom  {x} _ = x
+
+o<-cod :   { x y : Ordinal } → x o< y → Ordinal 
+o<-cod  {_} {y} _ = y
+
+o<-subst : {Z X z x : Ordinal }  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
+o<-subst df refl refl = df
+
+o<¬≡ :  { ox oy : Ordinal } → ox ≡ oy  → ox o< oy  → ⊥
+o<¬≡ {ox} {oy} eq lt with trio< ox oy
+o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
+o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
+o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
+
+o<> :   {x y : Ordinal   }  →  y o< x → x o< y → ⊥
+o<> {ox} {oy} lt tl with trio< ox oy
+o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
+o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
+o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
+
+osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
+osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
+osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
+osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
+
+osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
+----   y < osuc y < x < osuc x
+----   y < osuc y = x < osuc x
+----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
+osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
+osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
+osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
+osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with  osuc-≡< c
+osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
+osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
+
+osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox  
+osucprev {ox} {oy} oy<ox with trio< oy ox
+osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
+osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
+osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
+
+open _∧_
+
+osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
+proj2 (osuc2 x y) lt = osucc lt
+proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
+proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
+proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
+
+_o≤_ :  Ordinal → Ordinal → Set  n
+a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
+
+
+xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
+xo<ab   {oa} {ob} a→b with trio< oa ob
+xo<ab   {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
+xo<ab   {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
+xo<ab   {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
+
+maxα :   Ordinal  →  Ordinal  → Ordinal
+maxα x y with trio< x y
+maxα x y | tri< a ¬b ¬c = y
+maxα x y | tri> ¬a ¬b c = x
+maxα x y | tri≈ ¬a refl ¬c = x
+
+omin :    Ordinal  →  Ordinal  → Ordinal
+omin  x y with trio<  x  y
+omin x y | tri< a ¬b ¬c = x
+omin x y | tri> ¬a ¬b c = y
+omin x y | tri≈ ¬a refl ¬c = x
+
+min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
+min1  {x} {y} {z} z<x z<y with trio<  x y
+min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
+min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
+min1  {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
+
+--
+--  max ( osuc x , osuc y )
+--
+
+omax :  ( x y : Ordinal  ) → Ordinal 
+omax  x y with trio< x y
+omax  x y | tri< a ¬b ¬c = osuc y
+omax  x y | tri> ¬a ¬b c = osuc x
+omax  x y | tri≈ ¬a refl ¬c  = osuc x
+
+omax< :  ( x y : Ordinal  ) → x o< y → osuc y ≡ omax x y
+omax<  x y lt with trio< x y
+omax<  x y lt | tri< a ¬b ¬c = refl
+omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
+omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
+
+omax≤ :  ( x y : Ordinal  ) → x o≤ y → osuc y ≡ omax x y
+omax≤  x y le with trio< x y
+omax≤  x y le | tri< a ¬b ¬c = refl
+omax≤  x y le | tri≈ ¬a refl ¬c = refl
+omax≤  x y le | tri> ¬a ¬b c with osuc-≡< le
+omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
+omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)
+
+omax≡ :  ( x y : Ordinal  ) → x ≡ y → osuc y ≡ omax x y
+omax≡  x y eq with trio< x y
+omax≡  x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
+omax≡  x y eq | tri≈ ¬a refl ¬c = refl
+omax≡  x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
+
+omax-x :  ( x y : Ordinal  ) → x o< omax x y
+omax-x  x y with trio< x y
+omax-x  x y | tri< a ¬b ¬c = ordtrans a <-osuc
+omax-x  x y | tri> ¬a ¬b c = <-osuc
+omax-x  x y | tri≈ ¬a refl ¬c = <-osuc
+
+omax-y :  ( x y : Ordinal  ) → y o< omax x y
+omax-y  x y with  trio< x y
+omax-y  x y | tri< a ¬b ¬c = <-osuc
+omax-y  x y | tri> ¬a ¬b c = ordtrans c <-osuc
+omax-y  x y | tri≈ ¬a refl ¬c = <-osuc
+
+omxx :  ( x : Ordinal  ) → omax x x ≡ osuc x
+omxx  x with  trio< x x
+omxx  x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
+omxx  x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
+omxx  x | tri≈ ¬a refl ¬c = refl
+
+omxxx :  ( x : Ordinal  ) → omax x (omax x x ) ≡ osuc (osuc x)
+omxxx  x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
+
+open _∧_
+
+o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
+OrdTrans :  Transitive  _o≤_
+OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc
+
+OrdPreorder :   Preorder n n n
+OrdPreorder  = record { Carrier = Ordinal
+   ; _≈_  = _≡_ 
+   ; _∼_   = _o≤_
+   ; isPreorder   = record {
+        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
+        ; reflexive     = o≤-refl
+        ; trans         = OrdTrans 
+     }
+ }
+
+FExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
+  → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
+  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+  → ¬ p
+FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+
+nexto∅ : {x : Ordinal} → o∅ o< next x
+nexto∅ {x} with trio< o∅ x
+nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
+nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
+nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
+next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+next< {x} {y} {z} x<nz y<nx with trio< y (next z)
+next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
+next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
+   (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
+   (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+
+osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
+osuc< {x} {y} refl = <-osuc 
+
+nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
+nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
+
+nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
+nexto≡ {x} with trio< (next x) (next (osuc x) ) 
+--    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
+nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
+   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+nexto≡ {x} | tri≈ ¬a b ¬c = b
+--    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
+nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
+   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+
+next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
+next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
+    y<nx : y o< next x
+    y<nx = osuc< (sym eq)
+
+omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
+omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
+
+x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
+x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)    
+x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
+     ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
+x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
+     ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+
+≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
+≤next {x} {y} x≤y with trio< (next x) y
+≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
+≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
+≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x 
+
+x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
+x<ny→≤next {x} {y} x<ny with trio< x y
+x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
+x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
+x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
+
+omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
+omax<nomax {x} {y} with trio< x y
+omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
+omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+
+omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
+omax<nx {x} {y} {z} x<nz y<nz with trio< x y
+omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
+omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
+omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
+
+nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
+nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
+nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
+nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
+nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
+
+record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
+  field
+    os→ : (x : Ordinal) → x o< maxordinal → Ordinal
+    os← : Ordinal → Ordinal
+    os←limit : (x : Ordinal) → os← x o< maxordinal
+    os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
+    os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
+
+module o≤-Reasoning {n : Level}  (O : Ordinals {n} )  where
+
+    -- open inOrdinal O
+
+    resp-o< : _o<_ Respects₂ _≡_
+    resp-o< =  resp₂ _o<_
+
+    trans1 : {i j k : Ordinal} → i o< j → j o< osuc  k → i o< k
+    trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
+    trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
+    trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k
+
+    trans2 : {i j k : Ordinal} → i o< osuc j → j o<  k → i o< k
+    trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
+    trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
+    trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
+
+    open import Relation.Binary.Reasoning.Base.Triple 
+      (Preorder.isPreorder OrdPreorder) 
+         ordtrans --<-trans
+         (resp₂ _o<_) --(resp₂ _<_)
+         (λ x → ordtrans x <-osuc ) --<⇒≤
+         trans1 --<-transˡ
+         trans2 --<-transʳ
+         public
+         hiding (_≈⟨_⟩_)
+
diff -r 44a484f17f26 -r 9984cdd88da3 Ordinals.agda
--- a/Ordinals.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/Ordinals.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -20,12 +20,12 @@
 
 record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
-     Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
-     OTri : Trichotomous {n} _≡_  _o<_ 
-     ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
-     <-osuc :  { x : ord  } → x o< osuc x
-     osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-     Oprev-p :  ( x : ord  ) → Dec ( Oprev ord osuc x )
+     ordtrans : {x y z : ord }  → x o< y → y o< z → x o< z
+     trio<    : Trichotomous {n} _≡_  _o<_ 
+     ¬x<0     : { x : ord  } → ¬ ( x o< o∅  )
+     <-osuc   : { x : ord  } → x o< osuc x
+     osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
+     Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -41,316 +41,15 @@
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
-     ord : Set n
-     o∅ : ord
-     osuc : ord → ord
-     _o<_ : ord → ord → Set n
-     next :  ord → ord
-     isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
-     isNext : IsNext ord o∅ osuc _o<_ next
+     Ordinal : Set n
+     o∅ : Ordinal
+     osuc : Ordinal → Ordinal
+     _o<_ : Ordinal → Ordinal → Set n
+     next :  Ordinal → Ordinal
+     isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
+     isNext : IsNext Ordinal o∅ osuc _o<_ next
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
-        Ordinal : Set n
-        Ordinal  = Ordinals.ord O 
-
-        _o<_ :  Ordinal  → Ordinal  → Set n
-        _o<_ = Ordinals._o<_ O 
-
-        osuc :   Ordinal  → Ordinal 
-        osuc  = Ordinals.osuc O 
-
-        o∅ :   Ordinal  
-        o∅ = Ordinals.o∅ O
-
-        next :   Ordinal → Ordinal
-        next = Ordinals.next O
-
-        ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
-        osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
-        <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
-        TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
-        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
-        Oprev-p = IsOrdinals.Oprev-p  (Ordinals.isOrdinal O)
-
-        x<nx = IsNext.x<nx (Ordinals.isNext O)
-        osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
-        ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) 
-
-        o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
-        o<-dom  {x} _ = x
-
-        o<-cod :   { x y : Ordinal } → x o< y → Ordinal 
-        o<-cod  {_} {y} _ = y
-
-        o<-subst : {Z X z x : Ordinal }  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
-        o<-subst df refl refl = df
-
-        ordtrans :  {x y z : Ordinal  }   → x o< y → y o< z → x o< z
-        ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O)
-
-        trio< : Trichotomous  _≡_  _o<_ 
-        trio< = IsOrdinals.OTri (Ordinals.isOrdinal O)
-
-        o<¬≡ :  { ox oy : Ordinal } → ox ≡ oy  → ox o< oy  → ⊥
-        o<¬≡ {ox} {oy} eq lt with trio< ox oy
-        o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
-        o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
-        o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
-
-        o<> :   {x y : Ordinal   }  →  y o< x → x o< y → ⊥
-        o<> {ox} {oy} lt tl with trio< ox oy
-        o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
-        o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
-        o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
-
-        osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
-        osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
-        osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
-        osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
-
-        osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
-        ----   y < osuc y < x < osuc x
-        ----   y < osuc y = x < osuc x
-        ----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
-        osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
-        osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
-        osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
-        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with  osuc-≡< c
-        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
-        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
-
-        osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox  
-        osucprev {ox} {oy} oy<ox with trio< oy ox
-        osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
-        osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
-        osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
-
-        open _∧_
-
-        osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
-        proj2 (osuc2 x y) lt = osucc lt
-        proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
-        proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
-        proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
-
-        _o≤_ :  Ordinal → Ordinal → Set  n
-        a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
-
-
-        xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
-        xo<ab   {oa} {ob} a→b with trio< oa ob
-        xo<ab   {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
-        xo<ab   {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
-        xo<ab   {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
-
-        maxα :   Ordinal  →  Ordinal  → Ordinal
-        maxα x y with trio< x y
-        maxα x y | tri< a ¬b ¬c = y
-        maxα x y | tri> ¬a ¬b c = x
-        maxα x y | tri≈ ¬a refl ¬c = x
-
-        omin :    Ordinal  →  Ordinal  → Ordinal
-        omin  x y with trio<  x  y
-        omin x y | tri< a ¬b ¬c = x
-        omin x y | tri> ¬a ¬b c = y
-        omin x y | tri≈ ¬a refl ¬c = x
-
-        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
-        min1  {x} {y} {z} z<x z<y with trio<  x y
-        min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
-        min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
-        min1  {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
-
-        --
-        --  max ( osuc x , osuc y )
-        --
-
-        omax :  ( x y : Ordinal  ) → Ordinal 
-        omax  x y with trio< x y
-        omax  x y | tri< a ¬b ¬c = osuc y
-        omax  x y | tri> ¬a ¬b c = osuc x
-        omax  x y | tri≈ ¬a refl ¬c  = osuc x
-
-        omax< :  ( x y : Ordinal  ) → x o< y → osuc y ≡ omax x y
-        omax<  x y lt with trio< x y
-        omax<  x y lt | tri< a ¬b ¬c = refl
-        omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
-        omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
-
-        omax≤ :  ( x y : Ordinal  ) → x o≤ y → osuc y ≡ omax x y
-        omax≤  x y le with trio< x y
-        omax≤  x y le | tri< a ¬b ¬c = refl
-        omax≤  x y le | tri≈ ¬a refl ¬c = refl
-        omax≤  x y le | tri> ¬a ¬b c with osuc-≡< le
-        omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
-        omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)
-
-        omax≡ :  ( x y : Ordinal  ) → x ≡ y → osuc y ≡ omax x y
-        omax≡  x y eq with trio< x y
-        omax≡  x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
-        omax≡  x y eq | tri≈ ¬a refl ¬c = refl
-        omax≡  x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
-
-        omax-x :  ( x y : Ordinal  ) → x o< omax x y
-        omax-x  x y with trio< x y
-        omax-x  x y | tri< a ¬b ¬c = ordtrans a <-osuc
-        omax-x  x y | tri> ¬a ¬b c = <-osuc
-        omax-x  x y | tri≈ ¬a refl ¬c = <-osuc
-
-        omax-y :  ( x y : Ordinal  ) → y o< omax x y
-        omax-y  x y with  trio< x y
-        omax-y  x y | tri< a ¬b ¬c = <-osuc
-        omax-y  x y | tri> ¬a ¬b c = ordtrans c <-osuc
-        omax-y  x y | tri≈ ¬a refl ¬c = <-osuc
-
-        omxx :  ( x : Ordinal  ) → omax x x ≡ osuc x
-        omxx  x with  trio< x x
-        omxx  x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
-        omxx  x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
-        omxx  x | tri≈ ¬a refl ¬c = refl
-
-        omxxx :  ( x : Ordinal  ) → omax x (omax x x ) ≡ osuc (osuc x)
-        omxxx  x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
-
-        open _∧_
-
-        o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
-        o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
-        OrdTrans :  Transitive  _o≤_
-        OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
-        OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
-        OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
-        OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
-        OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc
-
-        OrdPreorder :   Preorder n n n
-        OrdPreorder  = record { Carrier = Ordinal
-           ; _≈_  = _≡_ 
-           ; _∼_   = _o≤_
-           ; isPreorder   = record {
-                isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-                ; reflexive     = o≤-refl
-                ; trans         = OrdTrans 
-             }
-         }
-
-        FExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
-          → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
-          → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-          → ¬ p
-        FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
-
-        nexto∅ : {x : Ordinal} → o∅ o< next x
-        nexto∅ {x} with trio< o∅ x
-        nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
-        nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
-        nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-
-        next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-        next< {x} {y} {z} x<nz y<nx with trio< y (next z)
-        next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
-        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
-           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
-        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
-           (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
-
-        osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
-        osuc< {x} {y} refl = <-osuc 
-
-        nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
-        nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
-
-        nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
-        nexto≡ {x} with trio< (next x) (next (osuc x) ) 
-        --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
-        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
-           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
-        nexto≡ {x} | tri≈ ¬a b ¬c = b
-        --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
-        nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
-           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
-
-        next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
-        next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
-            y<nx : y o< next x
-            y<nx = osuc< (sym eq)
-
-        omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
-        omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
-
-        x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
-        x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)    
-        x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
-             ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
-        x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
-        x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
-             ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
-
-        ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
-        ≤next {x} {y} x≤y with trio< (next x) y
-        ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
-        ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
-        ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
-        ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
-        ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x 
-
-        x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
-        x<ny→≤next {x} {y} x<ny with trio< x y
-        x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
-        x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
-        x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
-
-        omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
-        omax<nomax {x} {y} with trio< x y
-        omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
-        omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
-        omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
-
-        omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
-        omax<nx {x} {y} {z} x<nz y<nz with trio< x y
-        omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
-        omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
-        omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
-
-        nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
-        nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
-        nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
-        nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
-        nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
-
-        record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
-          field
-            os→ : (x : Ordinal) → x o< maxordinal → Ordinal
-            os← : Ordinal → Ordinal
-            os←limit : (x : Ordinal) → os← x o< maxordinal
-            os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
-            os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
-
-module o≤-Reasoning {n : Level} (O : Ordinals {n} )  where
-
-  open inOrdinal O
-
-  resp-o< : Ordinals._o<_ O Respects₂ _≡_
-  resp-o< =  resp₂ _o<_
-
-  trans1 : {i j k : Ordinal} → i o< j → j o< osuc  k → i o< k
-  trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
-  trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
-  trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k
-
-  trans2 : {i j k : Ordinal} → i o< osuc j → j o<  k → i o< k
-  trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
-  trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
-  trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
-
-  open import Relation.Binary.Reasoning.Base.Triple {n} {_} {_} {_} {Ordinal } {_≡_} {_o≤_} {_o<_}
-    (Preorder.isPreorder OrdPreorder) 
-    ordtrans --<-trans
-     (resp₂ _o<_) --(resp₂ _<_)
-    (λ x → ordtrans x <-osuc ) --<⇒≤
-    trans1 --<-transˡ
-    trans2 --<-transʳ
-    public
-    hiding (_≈⟨_⟩_)
-
+  open Ordinals O
+  open IsOrdinals 
diff -r 44a484f17f26 -r 9984cdd88da3 Todo
--- a/Todo	Sat Aug 01 11:06:29 2020 +0900
+++ b/Todo	Sat Aug 01 18:05:23 2020 +0900
@@ -1,6 +1,12 @@
+Sat Aug  1 13:16:53 JST 2020
+
+    P Generic Filter
+        as a ZF model 
+    define Definition for L
+
 Tue Jul 23 11:02:50 JST 2019
 
-    define cardinals 
+    define cardinals     ... done
     prove CH in OD→ZF
     define Ultra filter  ... done
     define L M : ZF ZFSet = M is an OD
diff -r 44a484f17f26 -r 9984cdd88da3 filter.agda
--- a/filter.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/filter.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -134,6 +134,12 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
+----
+--
+-- Filter/Ideal without ZF 
+--     L have to be a Latice
+--
+
 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
        filter : L → Set n
diff -r 44a484f17f26 -r 9984cdd88da3 ordinal.agda
--- a/ordinal.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/ordinal.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -1,13 +1,15 @@
 open import Level
 module ordinal where
 
-open import zf
-
+open import logic
+open import nat
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
-open import  Relation.Binary.PropositionalEquality
-open import  logic
-open import  nat
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties 
+open import Relation.Nullary
+open import Relation.Binary.Core
+
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -40,16 +42,6 @@
 d<→lv Φ< = refl
 d<→lv (s< lt) = refl
 
-o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
-o<-subst df refl refl = df
-
-open import Data.Nat.Properties 
-open import Data.Unit using ( ⊤ )
-open import Relation.Nullary
-
-open import Relation.Binary
-open import Relation.Binary.Core
-
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero }
 
@@ -207,14 +199,14 @@
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
 C-Ordinal {n} = record {
-     ord = Ordinal {suc n}
+     Ordinal = Ordinal {suc n}
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
    ; next = next
    ; isOrdinal = record {
-       Otrans = ordtrans
-     ; OTri = trio<
+       ordtrans = ordtrans
+     ; trio< = trio<
      ; ¬x<0 = ¬x<0 
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
diff -r 44a484f17f26 -r 9984cdd88da3 partfunc.agda
--- a/partfunc.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/partfunc.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -19,6 +19,10 @@
 open _∨_
 open Bool
 
+----
+--
+-- Partial Function without ZF
+--
 
 record PFunc  (Dom : Set n) (Cod : Set n) : Set (suc n) where
    field
@@ -26,6 +30,10 @@
       pmap : (x : Dom ) → dom x → Cod
       meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
 
+----
+--
+-- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
+--
 
 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
@@ -48,6 +56,10 @@
                        ; pmap = λ x y → find fp (lower x) (lower y)
                        ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} 
                        }
+----
+--
+-- to List (Maybe Two) is a Latice
+--
 
 _3⊆b_ : (f g : List (Maybe Two)) → Bool
 [] 3⊆b [] = true