# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558343923 -32400
# Node ID fce60b99dc55a12bb0da6e7fa52b21ada9aa2ab2
# Parent  f36e40d5d2c3811b05fea4a97cb8e356452b23b3
posturate OD is isomorphic to Ordinal

diff -r f36e40d5d2c3 -r fce60b99dc55 constructible-set.agda
--- a/constructible-set.agda	Sun May 19 18:13:42 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,246 +0,0 @@
-open import Level
-module constructible-set where
-
-open import zf
-
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-
-open import  Relation.Binary.PropositionalEquality
-
-data OrdinalD {n : Level} :  (lv : Nat) → Set n where
-   Φ : (lv : Nat) → OrdinalD  lv
-   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
-   ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)
-
-record Ordinal {n : Level} : Set n where
-   field
-     lv : Nat
-     ord : OrdinalD {n} lv
-
-data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
-   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
-   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
-   ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
-   ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  OSuc  (Suc lx) x d< (ℵ lx) 
-
-open Ordinal
-
-_o<_ : {n : Level} ( x y : Ordinal ) → Set n
-_o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
-
-open import Data.Nat.Properties 
-open import Data.Empty
-open import Relation.Nullary
-
-open import Relation.Binary
-open import Relation.Binary.Core
-
-o∅ : {n : Level} → Ordinal {n}
-o∅  = record { lv = Zero ; ord = Φ Zero }
-
-
-≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
-≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
-
-trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
-trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = 
-    trio<> s t
-
-trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
-trio<≡ refl = ≡→¬d<
-
-trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
-trio>≡ refl = ≡→¬d<
-
-triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
-triO  {n} {lx} {ly} x y = <-cmp lx ly
-
-triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
-triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
-triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  (ℵΦ<  {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
-triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ<  {_} {lv} {Φ (Suc lv)} )
-triOrdd  {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} )  ) (λ ()) (ℵ< {_} {lv} {y} )
-triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
-triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< )
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
-
-d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
-d<→lv Φ< = refl
-d<→lv (s< lt) = refl
-d<→lv ℵΦ< = refl
-d<→lv ℵ< = refl
-
-orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
-orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
-orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y}
-orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
-orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ<
-orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< ()
-orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< ()
-
-max : (x y : Nat) → Nat
-max Zero Zero = Zero
-max Zero (Suc x) = (Suc x)
-max (Suc x) Zero = (Suc x)
-max (Suc x) (Suc y) = Suc ( max x y )
-
-maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
-maxαd x y with triOrdd x y
-maxαd x y | tri< a ¬b ¬c = y
-maxαd x y | tri≈ ¬a b ¬c = x
-maxαd x y | tri> ¬a ¬b c = x
-
-maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-maxα x y with <-cmp (lv x) (lv y)
-maxα x y | tri< a ¬b ¬c = x
-maxα x y | tri> ¬a ¬b c = y
-maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
-
-_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
-a o≤ b  = (a ≡ b)  ∨ ( a o< b )
-
-ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
-ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
-ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
-... | refl = case1 x₁
-ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
-... | refl = case1 x₂
-ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
-... | refl | refl = case2 ( orddtrans x₁ x₂ )
-
-
-trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
-trio< a b with <-cmp (lv a) (lv b)
-trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
-   lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
-   lemma1 (case1 x) = ¬c x
-   lemma1 (case2 x) with d<→lv x
-   lemma1 (case2 x) | refl = ¬b refl
-trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
-   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
-   lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) with d<→lv x
-   lemma1 (case2 x) | refl = ¬b refl
-trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
-   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
-   lemma1 refl = refl
-   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
-   lemma2 (case1 x) = ¬a x
-   lemma2 (case2 x) = trio<> x a
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
-   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
-   lemma1 refl = refl
-   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
-   lemma2 (case1 x) = ¬a x
-   lemma2 (case2 x) = trio<> x c
-trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
-   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
-   lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) = ≡→¬d< x
-
-OrdTrans : {n : Level} → Transitive {suc n} _o≤_
-OrdTrans (case1 refl) (case1 refl) = case1 refl
-OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
-OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
-OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
-OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
-OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
-OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
-OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
-
-OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
-OrdPreorder {n} = record { Carrier = Ordinal
-   ; _≈_  = _≡_ 
-   ; _∼_   = _o≤_
-   ; isPreorder   = record {
-        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-        ; reflexive     = case1 
-        ; trans         = OrdTrans 
-     }
- }
-
-TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) 
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
-  →  ∀ (x : Ordinal)  → ψ x
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
-    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
-
--- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
-
--- Ordinal Definable Set
-
-record OD {n : Level}  : Set (suc n) where
-  field
-    α :  Ordinal {n}
-    def : (x : Ordinal {n} ) → x o< α → Set n
-
-open OD
-open import Data.Unit
-
-postulate      -- this is proved by Godel numbering of def
-   _c<_ : {n : Level } → (x y : OD {n} ) → Set (suc n)
-   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {suc n} _≡_ _c<_ 
-
--- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
--- o∋ a x x<A  = def a x x<A
-
--- TC u : Transitive Closure of OD u
---
---    all elements of u or elements of elements of u, etc...
---
--- TC Zero = u
--- TC (suc n) = ∪ (TC n)
---
--- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
--- 
---     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
---
--- Heritic Ordinal Definable
---
---    ( HOD = {x | TC x ⊆ OD } ) ⊆ OD
--- 
-
-HOD = OD
-
-c∅ : {n : Level} → HOD {n}
-c∅ {n} = record { α  = o∅ ; def = λ x y → Lift n ⊥ }
-
-HOD→ZF : {n : Level} → ZF {suc n} {suc n}
-HOD→ZF {n}  = record { 
-    ZFSet = HOD 
-    ; _∋_ = λ a b → b c< a
-    ; _≈_ = _≡_ 
-    ; ∅  = c∅
-    ; _,_ = _,_
-    ; Union = Union
-    ; Power = {!!}
-    ; Select = Select
-    ; Replace = Replace
-    ; infinite = {!!}
-    ; isZF = {!!}
- } where
-    Select : (X : HOD {n}) → (HOD {n} → Set (suc n)) → HOD {n}
-    Select X ψ = record { α = α X ; def = λ x →  {!!} } where 
-       select : Ordinal → Set n
-       select x with  ψ (record { α = x ; def = λ x → {!!} })
-       ... | t = Lift n ⊤
-    Replace : (X : HOD {n} ) → (HOD → HOD) → HOD
-    Replace X ψ  = record { α = {!!} ; def = λ x → {!!} }  
-    _,_ : HOD {n} → HOD → HOD
-    a , b  = record { α = maxα (α a) (α b) ; def = λ x x<ab → (   ) }  where
-       a∨b : Ordinal {suc n} → Set n
-       a∨b = {!!}
-    Union : HOD → HOD
-    Union a = {!!}
diff -r f36e40d5d2c3 -r fce60b99dc55 ordinal-definable.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ordinal-definable.agda	Mon May 20 18:18:43 2019 +0900
@@ -0,0 +1,151 @@
+open import Level
+module ordinal-definable where
+
+open import zf
+open import ordinal
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
+open import  Relation.Binary.PropositionalEquality
+
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+
+open import Relation.Binary
+open import Relation.Binary.Core
+
+
+-- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
+
+-- Ordinal Definable Set
+
+-- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
+-- o∋ a x x<A  = def a x x<A
+
+-- TC u : Transitive Closure of OD u
+--
+--    all elements of u or elements of elements of u, etc...
+--
+-- TC Zero = u
+-- TC (suc n) = ∪ (TC n)
+--
+-- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
+-- 
+--     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
+--
+-- Heritic Ordinal Definable
+--
+--    ( HOD = {x | TC x ⊆ OD } ) ⊆ OD     x ∈ OD here
+-- 
+
+record OD {n : Level}  : Set (suc n) where
+  field
+    def : (x : Ordinal {n} ) → Set n
+
+open OD
+open import Data.Unit
+
+postulate      
+  od→ord : {n : Level} → OD {n} → Ordinal {n}
+
+ord→od : {n : Level} → Ordinal {n} → OD {n} 
+ord→od x = record { def = λ y → x ≡ y }
+
+_∋_ : { n : Level } → ( a x : OD {n} ) → Set n
+_∋_ {n} a x  = def a ( od→ord x )
+
+_c<_ : { n : Level } → ( a x : OD {n} ) → Set n
+x c< a = a ∋ x 
+
+_c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
+a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
+
+postulate      
+  c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord x
+  o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od x
+  oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
+  diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+  sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
+  sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → ψ x  c< sup-od ψ
+
+HOD = OD
+
+od∅ : {n : Level} → HOD {n} 
+od∅ {n} = record { def = λ _ → Lift n ⊥ }
+
+∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
+∅1 {n} x (lift ())
+
+HOD→ZF : {n : Level} → ZF {suc n} {suc n}
+HOD→ZF {n}  = record { 
+    ZFSet = OD {n}
+    ; _∋_ = λ a x → Lift (suc n) ( a ∋ x )
+    ; _≈_ = _≡_ 
+    ; ∅  = od∅
+    ; _,_ = _,_
+    ; Union = Union
+    ; Power = Power
+    ; Select = Select
+    ; Replace = Replace
+    ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero  }  }
+    ; isZF = isZF 
+ } where
+    Replace : OD {n} → (OD {n} → OD {n} ) → OD {n}
+    Replace X ψ = sup-od ψ
+    Select : OD {n} → (OD {n} → Set (suc n) ) → OD {n}
+    Select X ψ = record { def = λ x → select ( ord→od x ) } where
+       select : OD {n} → Set n
+       select x with ψ x
+       ... | t =  Lift n ⊤
+    _,_ : OD {n} → OD {n} → OD {n}
+    x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
+    Union : OD {n} → OD {n}
+    Union x = record { def = λ y → {z : Ordinal {n}} → def x z  → def (ord→od z) y  }
+    Power : OD {n} → OD {n}
+    Power x = record { def = λ y → (z : Ordinal {n} ) → ( def x y ∧ def (ord→od z) y )  }
+    ZFSet = OD {n}
+    _∈_ : ( A B : ZFSet  ) → Set n
+    A ∈ B = B ∋ A
+    _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set n
+    _⊆_ A B {x} = A ∋ x →  B ∋ x
+    _∩_ : ( A B : ZFSet  ) → ZFSet
+    A ∩ B = Select (A , B) (  λ x → (Lift (suc n) ( A ∋ x )) ∧ (Lift (suc n) ( B ∋ x )  ))
+    _∪_ : ( A B : ZFSet  ) → ZFSet
+    A ∪ B = Select (A , B) (  λ x → (Lift (suc n) ( A ∋ x )) ∨ (Lift (suc n) ( B ∋ x )  ))
+    infixr  200 _∈_
+    infixr  230 _∩_ _∪_
+    infixr  220 _⊆_
+    isZF : IsZF (OD {n})  (λ a x → Lift (suc n) ( a ∋ x )) _≡_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero }  })
+    isZF = record {
+           isEquivalence  = record { refl = refl ; sym = sym ; trans = trans }
+       ;   pair  = pair
+       ;   union→ = {!!}
+       ;   union← = {!!}
+       ;   empty = empty
+       ;   power→ = {!!}
+       ;   power← = {!!}
+       ;   extentionality = {!!}
+       ;   minimul = {!!}
+       ;   regularity = {!!}
+       ;   infinity∅ = {!!}
+       ;   infinity = {!!}
+       ;   selection = {!!}
+       ;   replacement = {!!}
+     } where
+         open _∧_ 
+         pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B)
+         proj1 (pair A B ) = lift ( case1 refl )
+         proj2 (pair A B ) = lift ( case2 refl )
+         empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x)
+         empty x (lift (lift ()))
+         union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y)
+         union→ X x y (lift X∋x) (lift x∋y) = lift lemma  where
+            lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
+            lemma {z} X∋z = {!!}
+
+
+
+
+
+
diff -r f36e40d5d2c3 -r fce60b99dc55 ordinal.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ordinal.agda	Mon May 20 18:18:43 2019 +0900
@@ -0,0 +1,179 @@
+open import Level
+module ordinal where
+
+open import zf
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
+open import  Relation.Binary.PropositionalEquality
+
+data OrdinalD {n : Level} :  (lv : Nat) → Set n where
+   Φ : (lv : Nat) → OrdinalD  lv
+   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+   ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)
+
+record Ordinal {n : Level} : Set n where
+   field
+     lv : Nat
+     ord : OrdinalD {n} lv
+
+data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
+   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
+   ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
+   ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  OSuc  (Suc lx) x d< (ℵ lx) 
+
+open Ordinal
+
+_o<_ : {n : Level} ( x y : Ordinal ) → Set n
+_o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
+
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+
+open import Relation.Binary
+open import Relation.Binary.Core
+
+o∅ : {n : Level} → Ordinal {n}
+o∅  = record { lv = Zero ; ord = Φ Zero }
+
+
+≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
+≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
+
+trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
+trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = 
+    trio<> s t
+
+trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
+trio<≡ refl = ≡→¬d<
+
+trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
+trio>≡ refl = ≡→¬d<
+
+triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
+triO  {n} {lx} {ly} x y = <-cmp lx ly
+
+triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
+triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
+triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  (ℵΦ<  {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
+triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ<  {_} {lv} {Φ (Suc lv)} )
+triOrdd  {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} )  ) (λ ()) (ℵ< {_} {lv} {y} )
+triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
+triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< )
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
+triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
+
+d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
+d<→lv Φ< = refl
+d<→lv (s< lt) = refl
+d<→lv ℵΦ< = refl
+d<→lv ℵ< = refl
+
+orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
+orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
+orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y}
+orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
+orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ<
+orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< ()
+orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< ()
+
+max : (x y : Nat) → Nat
+max Zero Zero = Zero
+max Zero (Suc x) = (Suc x)
+max (Suc x) Zero = (Suc x)
+max (Suc x) (Suc y) = Suc ( max x y )
+
+maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
+maxαd x y with triOrdd x y
+maxαd x y | tri< a ¬b ¬c = y
+maxαd x y | tri≈ ¬a b ¬c = x
+maxαd x y | tri> ¬a ¬b c = x
+
+maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
+maxα x y with <-cmp (lv x) (lv y)
+maxα x y | tri< a ¬b ¬c = x
+maxα x y | tri> ¬a ¬b c = y
+maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+
+_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
+a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+
+ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
+ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+... | refl = case1 x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+... | refl = case1 x₂
+ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
+... | refl | refl = case2 ( orddtrans x₁ x₂ )
+
+
+trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
+trio< a b with <-cmp (lv a) (lv b)
+trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
+   lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
+   lemma1 (case1 x) = ¬c x
+   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) | refl = ¬b refl
+trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
+   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) with d<→lv x
+   lemma1 (case2 x) | refl = ¬b refl
+trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x a
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
+   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
+   lemma1 refl = refl
+   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
+   lemma2 (case1 x) = ¬a x
+   lemma2 (case2 x) = trio<> x c
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
+   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
+   lemma1 (case1 x) = ¬a x
+   lemma1 (case2 x) = ≡→¬d< x
+
+OrdTrans : {n : Level} → Transitive {suc n} _o≤_
+OrdTrans (case1 refl) (case1 refl) = case1 refl
+OrdTrans (case1 refl) (case2 lt2) = case2 lt2
+OrdTrans (case2 lt1) (case1 refl) = case2 lt1
+OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
+OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
+OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
+OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
+OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
+OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
+OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
+
+OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
+OrdPreorder {n} = record { Carrier = Ordinal
+   ; _≈_  = _≡_ 
+   ; _∼_   = _o≤_
+   ; isPreorder   = record {
+        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
+        ; reflexive     = case1 
+        ; trans         = OrdTrans 
+     }
+ }
+
+TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
+    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+
diff -r f36e40d5d2c3 -r fce60b99dc55 set-of-agda.agda
--- a/set-of-agda.agda	Sun May 19 18:13:42 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-module set-of-agda where
-
-open import Level
-open import Data.Bool
-
--- infix  50 _∧_
-
--- record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
---    constructor _×_
---    field 
---       proj1 : A
---       proj2 : B
-
--- open _∧_
-
--- infix  50 _∨_
-
--- data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
---    case1 : A → A ∨ B
---    case2 : B → A ∨ B
-
-data ZFSet {n : Level} : Set (suc (suc n)) where
-    elem : { A : Set  n } ( a : A ) → ZFSet 
-    ∅ : ZFSet  {n}
-    pair : {A B : Set n} (a : A ) (b : B ) → ZFSet 
-    union :  (A  : Set (suc n) ) → ZFSet  
-    -- repl :  ( ψ : ZFSet {n} →  Set zero )   → ZFSet 
-    infinite : ZFSet 
-    power : (A  : ZFSet {n})  → ZFSet 
-
-infix  60 _∋_ _∈_
-
-open import Relation.Binary.PropositionalEquality 
-
-data _∈_ {n : Level} : {A : Set n}  ( a : A )  ( Z : ZFSet {n} )  → Set (suc n) where
-    ∈-elm : {A : Set n } {a : A} →  a ∈ (elem a)   
-    ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A}  → a ∈  (pair a b)   
-    ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B}  → b ∈  (pair a b)   
---    ∈-union : {Z : Set (suc n)}  {A : Z }  → {a : {!!} } → a ∈ (union Z)  
---    ∈-repl : {A : Set n } { B : Set n}  → { ψ : B → A } → { b : B } → ψ b ∈  {!!} -- (repl {!!}) 
-    -- ∈-infinite-1 : ∅ ∈ infinite 
---    ∈-infinite : {A : Set n} {a : A} → _∈_  infinite {A} a 
-    ∈-power : {A B : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈  (power Z)  
-
--- _∈_  : {n : Level} { A : ZFSet {n} } → {B : Set n} →  (a : B ) →  Set n  → Bool
--- _∈_ {_} {A} a _  = A ∋ a
-
-infix  40 _⇔_
-
--- _⇔_ : {n : Level} (A  B : Set n)  → Set  n 
--- A ⇔ B = ( ∀ {x : A } → x ∈ B  ) ∧  ( ∀ {x : B } → x ∈ A )
-
--- Axiom of extentionality
--- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ]
-
--- set-extentionality : {n : Level } {x y : Set n }  → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n))  → ( x ∈ w ⇔ y ∈ w ) 
--- proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x )
--- proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y )
-
-
-open import Relation.Nullary
-open import Data.Empty
-
--- data ∅  : Set where
-
-infix  50 _∩_
-
--- record _∩_ {n m : Level} (A : Set n) ( B : Set m)  : Set (n ⊔ m) where
---    field
---       inL : {x : A } → x ∈ A
---       inR : {x : B } → x ∈ B
-
--- open _∩_
-
--- lemma : {n m : Level} (A : Set n) ( B : Set m) → (a : A ) → a ∈ (A ∩ B) 
--- lemma A B a A∩B = inL A∩B
-
--- Axiom of regularity 
--- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-
--- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x  ⇔ ∅ )
--- set-regularity = {!!}
-
---  Axiom of pairing
--- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z).
-
--- pair : {n m : Level}  ( x : Set n ) ( y : Set m ) → Set (n ⊔ m)
--- pair x y = {!!} -- ( x × y )
-
--- Axiom of Union
--- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t  ∈ x))
-
--- axiom of infinity
--- ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
-
--- axiom of replacement
--- ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
-
--- axiom of power set
--- ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 
-
-
-
-
diff -r f36e40d5d2c3 -r fce60b99dc55 zf.agda
--- a/zf.agda	Sun May 19 18:13:42 2019 +0900
+++ b/zf.agda	Mon May 20 18:18:43 2019 +0900
@@ -55,7 +55,7 @@
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
   field
-     isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ 
+     isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 
      -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
      pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
      -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t  ∈ x))