# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562027306 -32400
# Node ID 2a5519dcc1677b671a8ff3f9c5accc84c2539515
# Parent  69a845b82854fb5cee4dd5ecd432d47e0721ba83
ord power set

diff -r 69a845b82854 -r 2a5519dcc167 HOD.agda
--- a/HOD.agda	Mon Jul 01 19:13:43 2019 +0900
+++ b/HOD.agda	Tue Jul 02 09:28:26 2019 +0900
@@ -60,9 +60,9 @@
   -- HOD can be iso to a subset of Ordinal ( by means of Godel Set )
   od→ord : {n : Level} → HOD {n} → Ordinal {n}
   ord→od : {n : Level} → Ordinal {n} → HOD {n} 
+  c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   oiso   : {n : Level} {x : HOD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
-  c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
   ==→o≡ : {n : Level} →  { x y : HOD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
@@ -243,6 +243,19 @@
 Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
+OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
+OrdSubset {n} A x = ===-≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+  lemma1 :  {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y
+  lemma1 {y} s with trio< A x
+  lemma1 {y} s | tri< a ¬b ¬c = proj1 s
+  lemma1 {y} s | tri≈ ¬a refl ¬c = proj1 s
+  lemma1 {y} s | tri> ¬a ¬b c = proj2 s
+  lemma2 : {y : Ordinal} → def (Ord (minα A x)) y → def (ZFSubset (Ord A) (Ord x)) y
+  lemma2 {y} lt with trio< A x
+  lemma2 {y} lt | tri< a ¬b ¬c = record { proj1 = lt ; proj2 = ordtrans lt a }
+  lemma2 {y} lt | tri≈ ¬a refl ¬c = record { proj1 = lt ; proj2 = lt }
+  lemma2 {y} lt | tri> ¬a ¬b c = record { proj1 = ordtrans lt c ; proj2 = lt }
+
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
 -- L (Φ 0) = Φ
@@ -296,8 +309,6 @@
     Union : HOD {suc n} → HOD {suc n}
     Union U = cseq U 
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
-    Power : HOD {suc n} → HOD {suc n}
-    Power A = Def A
     ZFSet = HOD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
@@ -305,6 +316,8 @@
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
+    Power : HOD {suc n} → HOD {suc n}
+    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     ｛_｝ : ZFSet → ZFSet
@@ -321,7 +334,7 @@
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
-       ;   power→ = power→
+       ;   power→ = power→  
        ;   power← = power← 
        ;   extensionality = extensionality
        ;   minimul = minimul
@@ -331,12 +344,15 @@
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement = replacement
      } where
+
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
+
          empty : (x : HOD {suc n} ) → ¬  (od∅ ∋ x)
          empty x (case1 ())
          empty x (case2 ())
+
          ---
          --- 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
@@ -345,37 +361,60 @@
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
          --
-         POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t)
-         POrd {A} {t} P∋t = o<→c< P∋t
-         power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x with osuc-≡<  (sup-lb  (POrd P∋t))
+         POrd : {a : Ordinal } {t : HOD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
+         POrd {a} {t} P∋t = o<→c< P∋t
+         ord-power→ : (a : Ordinal ) ( t : HOD) → Def (Ord a) ∋ t → {x : HOD} → t ∋ x → Ord a ∋ x
+         ord-power→ a t P∋t {x} t∋x with osuc-≡<  (sup-lb  (POrd P∋t))
          ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  where
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
-         ... | case2 lt = otrans A (proj1 (lemma1 lt) )
+         ... | case2 lt = otrans (Ord a) (proj1 (lemma1 lt) )
                    (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where
+              sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
               minsup :  HOD
-              minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
+              minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
-              lemma1 lt = {!!}
+              lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
+              ... | eq with subst ( λ k →  ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq
+              ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} (o<→c< lt) lemma2 (sym ord-Ord) where
+                  lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup
+                  lemma2 =  let open ≡-Reasoning in begin
+                      Ord (od→ord (ZFSubset (Ord a) (ord→od sp)))
+                    ≡⟨ cong (λ k → Ord (od→ord k)) eq1 ⟩
+                      Ord (od→ord (Ord (minα a sp))) 
+                    ≡⟨ cong (λ k → Ord (od→ord k)) Ord-ord  ⟩
+                      Ord (od→ord (ord→od (minα a sp))) 
+                    ≡⟨ cong (λ k → Ord k) diso ⟩
+                      Ord (minα a sp)
+                    ≡⟨ sym eq1 ⟩
+                      minsup
+                    ∎
+
          -- 
          -- 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 : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
+         ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
+         ord-power← a t t→A  = def-subst {suc n} {_} {_} {Def (Ord a)} {od→ord t}
                  lemma refl (lemma1 lemma-eq )where
-              lemma-eq :  ZFSubset A t == t
+              lemma-eq :  ZFSubset (Ord 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}
+                 proj1 = def-subst {suc n} {_} {_} {(Ord a)} {z}
                     ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 : {n : Level } { A t : HOD {suc n}} → (eq : ZFSubset A t == t)  → od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 {n} {A} {t} eq = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
-              lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
+              lemma1 : {n : Level } {a : Ordinal {suc n}} { t : HOD {suc n}}
+                 → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
+              lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
+
+         power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
+         power→ = {!!}
+         power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+         power← = {!!}
+
          union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
          union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
@@ -388,6 +427,7 @@
          union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
              lemma : X ∋ union-u {X} {z} X∋z
              lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
+
          ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
@@ -395,8 +435,10 @@
              proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
            ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
                                   ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
+
          replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = sup-c< ψ {x}
+
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          regularity :  (x : HOD) (not : ¬ (x == od∅)) →
@@ -409,9 +451,11 @@
                  lemma3 = proj1 s x₁ (proj2 s)
              lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
              lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
+
          extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+
          open  import  Relation.Binary.PropositionalEquality
          uxxx-ord : {x  : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
          uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x))  where
diff -r 69a845b82854 -r 2a5519dcc167 ordinal.agda
--- a/ordinal.agda	Mon Jul 01 19:13:43 2019 +0900
+++ b/ordinal.agda	Tue Jul 02 09:28:26 2019 +0900
@@ -216,17 +216,24 @@
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
 
-maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-maxα x y with <-cmp (lv x) (lv y)
+maxα : {n : Level} →  Ordinal {suc n} →  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 = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+maxα x y | tri≈ ¬a refl ¬c = x
 
-minα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-minα x y with <-cmp (lv x) (lv y)
+minα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
+minα {n} x y with trio< {n} x  y
 minα x y | tri< a ¬b ¬c = x
 minα x y | tri> ¬a ¬b c = y
-minα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = minαd (ord x) (ord y) }
+minα x y | tri≈ ¬a refl ¬c = x
+
+min1 : {n : Level} →  {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y
+min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
+min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
+min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
+min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
+
 --
 --  max ( osuc x , osuc y )
 --