# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592878470 -32400
# Node ID 3795ffb127d02ba7a525ae32ffd61eb384948f3e
# Parent  be6670af87fa32a81179eb4ccf1378b1e6cb8892
... should we use HOD?

diff -r be6670af87fa -r 3795ffb127d0 OD.agda
--- a/OD.agda	Mon Jun 22 16:43:31 2020 +0900
+++ b/OD.agda	Tue Jun 23 11:14:30 2020 +0900
@@ -73,7 +73,9 @@
   maxod : Ordinal
   od→ord : OD  → Ordinal 
   ord→od : (x : Ordinal ) → x o< maxod  → OD  
+  -- ZFSet has bounded solution of OD
   o<max : {x : OD } → od→ord x o< maxod  
+  def<maxod : {x y : Ordinal} → (lt : x o< maxod) → def (ord→od x lt ) y → y o< maxod
   c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
   oiso   :  {x : OD }      → ord→od ( od→ord x ) o<max ≡ x
   diso   :  {x : Ordinal } → (lt : x o< maxod)   → od→ord ( ord→od x lt ) ≡ x
@@ -107,6 +109,7 @@
 od∅  = Ord o∅ 
 
 
+-- = subst (λ k → k o< maxod ) (diso {!!}) ( ordtrans ( c<→o< lt ) o<max   )
 -- o<→c<→OD=Ord : ( {x y : Ordinal  } → x o< y → def (ord→od y {!!} ) x ) → {x : OD } →  x ≡ Ord (od→ord x)
 -- o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
 --    lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
@@ -143,11 +146,6 @@
 --     lemma : x o< maxod
 --     lemma = subst (λ k → k o< maxod ) (diso {!!} ) (otrans o<max ( c<→o< lt ))
 
-
--- avoiding lv != Zero error
-orefl : { x : OD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
-orefl refl = refl
-
 ==-iso : { x y : OD  } → ord→od (od→ord x) o<max == ord→od (od→ord y) o<max →  x == y
 ==-iso  {x} {y} eq = record {
       eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
@@ -159,28 +157,37 @@
 =-iso :  {x y : OD  } → (x == y) ≡ (ord→od (od→ord x) o<max == y)
 =-iso  {_} {y} = cong ( λ k → k == y ) (sym oiso)
 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
+-- 
 <-irr : {x y z : Ordinal } → x ≡ y → (x o< z) ≡ (y o< z)
 <-irr refl = refl
 
 ord→== : { x y : OD  } → od→ord x ≡  od→ord y →  x == y
-ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq) o<max o<max ) where
+ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) eq o<max o<max ) where
     lemma : ( ox oy : Ordinal  ) → ox ≡ oy → (x<m : ox o< maxod) (y<m : oy o< maxod)  →  (ord→od ox x<m ) == (ord→od oy y<m )
     lemma ox ox  refl x<m y<m = subst (λ  k → ord→od ox x<m == ord→od ox k) {!!} ==-refl
 
-o≡→== : { x y : Ordinal  } → x ≡ y →  ord→od x {!!} == ord→od y {!!}
-o≡→==  {x} {.x} refl = ==-refl
+o≡→== : { x y : Ordinal  } → x ≡ y → (lx : x o< maxod ) → (ly : y o< maxod )  →  ord→od x lx == ord→od y ly 
+o≡→==  {x} {.x} refl _ _ = {!!} -- ==-refl
 
-o∅≡od∅ : ord→od (o∅ ) {!!} ≡ od∅ 
+o∅<maxod : o∅ o< maxod 
+o∅<maxod with IsOrdinals.OTri (Ordinals.isOrdinal O)  o∅ maxod
+o∅<maxod | tri< a ¬b ¬c = a
+o∅<maxod | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 (subst (λ k → (od→ord record { def = λ x → One }) o< k ) (sym b) o<max ))
+o∅<maxod | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) 
+
+o∅≡od∅ : ord→od o∅ o∅<maxod ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
-     lemma0 :  {x : Ordinal} → def (ord→od o∅ {!!} ) x → def od∅ x
-     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x {!!} } {ord→od o∅ {!!} } (def-subst  {ord→od o∅ {!!} } {x} lt refl (sym (diso {!!} ))) ) (diso {!!}) (diso {!!})
-     lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅ {!!} ) x
+     lemma0 :  {x : Ordinal} → x o< maxod  → def (ord→od o∅ o∅<maxod) x → def od∅ x
+     lemma0 {x} x<m lt = o<-subst (c<→o<  {ord→od x x<m } {ord→od o∅ o∅<maxod}
+        (def-subst  {ord→od o∅ o∅<maxod} {x} lt refl (sym (diso x<m ))) ) (diso x<m) (diso o∅<maxod)
+     lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅ o∅<maxod ) x
      lemma1 {x} lt = ⊥-elim (¬x<0 lt)
-     lemma : ord→od o∅ {!!} == od∅
-     lemma = record { eq→ = lemma0 ; eq← = lemma1 }
+     lemma : ord→od o∅ o∅<maxod == od∅
+     lemma = record { eq→ = λ {x} lt → lemma0 (def<maxod o∅<maxod lt ) lt ; eq← = lemma1 }
 
 ord-od∅ : od→ord (od∅ ) ≡ o∅ 
-ord-od∅  = sym ( subst (λ k → k ≡  od→ord (od∅ ) ) (diso {!!}) (cong ( λ k → od→ord k ) o∅≡od∅ ) )
+ord-od∅  = sym ( subst (λ k → k ≡  od→ord (od∅ ) ) (diso o∅<maxod) (cong ( λ k → od→ord k ) o∅≡od∅ ) )
 
 ∅0 : record { def = λ x →  Lift n ⊥ } == od∅  
 eq→ ∅0 {w} (lift ())
@@ -208,8 +215,9 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
+
 in-codomain : (X : OD  ) → ( ψ : OD  → OD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y {!!} )))))  }
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (lt : def X y ) → (lt : y o< maxod)  →  ( x ≡ od→ord (ψ (ord→od y lt )))))  } where
 
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
@@ -312,8 +320,8 @@
      } where
 
          pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) 
-         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
-         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
+         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x {!!} {!!} ))
+         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y {!!} {!!} ))
 
          pair← : ( x y t : ZFSet  ) → ( t == x ) ∨ ( t == y ) →  (x , y)  ∋ t  
          pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
@@ -350,14 +358,14 @@
          replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
          replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
              lemma : def (in-codomain X ψ) (od→ord (ψ x))
-             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
+             lemma not = ⊥-elim ( not ( od→ord x ) {!!} ) -- (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
             lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} ))))
                     → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )))
             lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
                 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))  
-                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq )
+                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq {!!} {!!} )
             lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) )
             lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso  ( proj2 not2 ))
 
@@ -433,7 +441,7 @@
               lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ x)))
                   lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
-              lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
+              lemma2 not = ⊥-elim ( not (od→ord t) {!!}) where -- (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t) {!!} ) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))