# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1560655578 -32400
# Node ID c31ac67e9ecb58358442039bcfc4a0e46fb8be89
# Parent  ec6235ce021579bb1604a40fafc96b5d63e63e50
add Ord Ordinal order preserving map

diff -r ec6235ce0215 -r c31ac67e9ecb ordinal-definable.agda
--- a/ordinal-definable.agda	Sun Jun 16 11:37:00 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 16 12:26:18 2019 +0900
@@ -72,11 +72,9 @@
 _c<_ : { n : Level } → ( x a : Ordinal {n} ) → Set n
 _c<_ {n} x  a = Ord {n} a ∋ Ord x
 
-c<→o< : { n : Level } → { x a : OD {n} } → record { def = λ y → y o< od→ord a } ∋ x → od→ord x o< od→ord a
-c<→o< lt = lt
-
-o<→c< : { n : Level } → { x a : OD {n} } → od→ord x o< od→ord a → record { def = λ y → y o< od→ord a } ∋ x 
-o<→c< lt = lt
+postulate      
+   c<→o< : { n : Level } → { x a : Ordinal {n} } → Ord a  ∋ Ord x →  x o<  a
+   o<→c< : { n : Level } → { x a : Ordinal {n} } → x o< a → Ord a ∋ Ord x 
 
 ==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } →  Ord x == Ord y →  x ≡ y 
 ==→o≡ {n} {x} {y} eq with trio< {n} x y
@@ -131,7 +129,7 @@
 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {record { def = λ y → y o< ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) }} {od→ord ( ψ x )}
         lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
     lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
-    lemma = subst₂ (λ j k → j o< k ) refl diso (o<→c< (o<-subst sup-o< refl (sym diso) ) )
+    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso)  )
 
 ∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
@@ -165,6 +163,10 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
 
+transitive-Ord : {n : Level } { z y x : Ordinal {suc n} } → Ord z ∋ Ord y → Ord y ∋ Ord x → Ord z  ∋ Ord x
+transitive-Ord = {!!}
+
+
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
@@ -324,6 +326,16 @@
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x (case1 ())
          empty x (case2 ())
+
+         power→Ord : (A t : Ordinal) → Power (Ord A) ∋ (Ord t) → {x : OD} → Ord t ∋ x → Ord A ∋ x
+         power→Ord A t P∋t {x} t∋x = {!!} where
+              minsup :  OD
+              minsup =  ZFSubset (Ord A) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord A) (ord→od x))))) 
+              lemma-t : csuc minsup ∋ Ord t
+              lemma-t with  sup-lb {!!}
+              ... | c = {!!}
+         power←Ord : (A t : Ordinal) → ({x : OD} → (Ord t ∋ x → Ord A ∋ x)) → Power (Ord A) ∋ Ord t
+         power←Ord = {!!}
          ---
          --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
          --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
@@ -333,42 +345,17 @@
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
          --
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = proj1 lemma-s where
-              minsup :  OD
-              minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
-              lemma-t : csuc minsup ∋ t
-              lemma-t = {!!}
-              lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
-              lemma-s = {!!}
+         power→ A t P∋t {x} t∋x = {!!}
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
          -- 
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
-                  {!!} refl lemma1 where
-              lemma-eq :  ZFSubset A t == t
-              eq→ lemma-eq {z} w = proj2 w 
-              eq← lemma-eq {z} w = record { proj2 = w  ;
-                 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
-              lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
-              lemma = sup-o<   
-         union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
-         union-lemma-u {X} {z} U>z = lemma <-osuc where
-             lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
-             lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} {!!} refl refl
+         power← A t t→A  = {!!}
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-         union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
-         union→ X y u xx | tri< a ¬b ¬c with  osuc-< a {!!}
-         union→ X y u xx | tri< a ¬b ¬c | ()
-         union→ X y u xx | tri≈ ¬a b ¬c = lemma b {!!} where
-             lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
-             lemma refl lt = lt
-         union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c {!!} 
+         union→ = {!!}
          union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
-         union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
+         union← = {!!}
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)