# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562582123 -32400
# Node ID c848550c8b39bf4e616d22a6707a1bdcbf9c8a8f
# Parent  2eafa89733ed584d7c8959d2b8cfb107066be23f
...

diff -r 2eafa89733ed -r c848550c8b39 HOD.agda
--- a/HOD.agda	Mon Jul 08 18:26:33 2019 +0900
+++ b/HOD.agda	Mon Jul 08 19:35:23 2019 +0900
@@ -60,7 +60,6 @@
   c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   oiso   : {n : Level} {x : OD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
-  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
   ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
@@ -78,12 +77,6 @@
   -- we should prove this in agda, but simply put here
   ===-≡ : {n : Level} { x y : OD {suc n}} → x == y  → x ≡ y
 
-Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox
-Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord)) 
-
-Ord-ord-≡ : {n : Level } {t : OD {suc n}} → Ord (od→ord t) ≡ t
-Ord-ord-≡ {n} {t}  = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k) (sym ord-Ord))
-
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
@@ -99,12 +92,6 @@
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 
-o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt 
-
-o<→c<'  : {n : Level} {x y : OD {suc n} } → od→ord x o< od→ord y → y ∋ x 
-o<→c<' {n} {x} {y} lt = def-subst {suc n} {Ord (od→ord y)} {od→ord x} {y} {od→ord x} lt Ord-ord-≡ refl
-
 sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
 
@@ -114,20 +101,6 @@
     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<-subst sup-o< refl (sym diso)  )
 
-o<→o> : {n : Level} →  { x y : Ordinal {n} } →  (Ord x == Ord y) → x o< y → ⊥
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with o<-subst (yx (case1 lt)) ord-Ord refl
-... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
-... | ()
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with  o<-subst (yx (case2 lt)) ord-Ord refl
-... | oyx with o<¬≡ refl (c<→o< {n} {Ord x} oyx )
-... | ()
-
-Ord==→≡ : {n : Level} { x y : Ordinal {suc n}} → Ord x == Ord y → x ≡ y
-Ord==→≡ {n} {x} {y} eq with trio< x y
-Ord==→≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq a )
-Ord==→≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
-Ord==→≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) c )
-
 otrans : {n : Level} {a x : Ordinal {n} } → def (Ord a) x → { y : Ordinal {n} } → y o< x → def (Ord a) y
 otrans {n} {a} {x} x<a {y} y<x = ordtrans y<x x<a
 
@@ -194,8 +167,7 @@
 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
     lemma :  o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
-    lemma lt with o<→c< lt 
-    lemma lt | t = o<¬≡ refl t
+    lemma lt = {!!}
 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
@@ -267,14 +239,6 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
     cseq ( Ord (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }))))
 
-L00 :   {n : Level} → (ox : Ordinal {suc n}) → ox o<  sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))
-L00 {n} ox =  o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))}
-  (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl where
-      lemma1 : {n : Level } {ox z : Ordinal {suc n}} → ( def (Ord ox) z ∧ def (ord→od ox) z ) ⇔ def ( Ord ox ) z
-      lemma1 {n} {ox} {z} = record { proj1 = proj1 ; proj2 = λ t → record { proj1 = t ; proj2 = subst (λ k → def k z ) Ord-ord t }}
-      lemma0 :  {n : Level} → (ox : Ordinal {suc n}) →  od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox
-      lemma0 {n} ox = trans (cong (λ k → od→ord k) (===-≡ (⇔→== lemma1) )) (sym ord-Ord)
-
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
@@ -357,7 +321,7 @@
          union→ X z u xx | tri≈ ¬a b ¬c =  def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b
          union→ X z u xx | tri> ¬a ¬b c =  def-subst lemma1 (sym lemma0) diso where
              lemma0 : X ≡ Ord (od→ord X)
-             lemma0 = sym Ord-ord-≡
+             lemma0 = sym {!!}
              lemma : osuc (od→ord z) o< od→ord X
              lemma = ordtrans c ( c<→o< ( proj1 xx ) )
              lemma1 : Ord ( od→ord X) ∋ ord→od (osuc (od→ord z) )
@@ -365,7 +329,7 @@
          union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z UX∋z = record { proj1 = lemma ; proj2 = <-osuc } where
              lemma : X ∋ union-u {X} {z} UX∋z
-             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl ord-Ord
+             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!}
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
@@ -378,7 +342,7 @@
          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 (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
+                 (sym (subst (λ k → Ord (od→ord x) ≡ k) 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
             lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
@@ -402,7 +366,7 @@
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
          --
          POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
-         POrd {a} {t} P∋t = o<→c< P∋t
+         POrd {a} {t} P∋t = {!!}
          ∩-≡ :  { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
          ∩-≡ {a} {b} inc = record {
             eq→ = λ {x} x<a → record { proj2 = x<a ;
@@ -422,14 +386,14 @@
               -- lemma1 hold because minsup is Ord (minα a sp) 
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
               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
+              ... | eq with subst ( λ k →  ZFSubset (Ord a) k ≡ Ord (minα a sp)) {!!} eq
+              ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} {!!} lemma2 {!!} 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  ⟩
+                    ≡⟨ cong (λ k → Ord (od→ord k)) {!!}  ⟩
                       Ord (od→ord (ord→od (minα a sp))) 
                     ≡⟨ cong (λ k → Ord k) diso ⟩
                       Ord (minα a sp)
@@ -480,12 +444,12 @@
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
               lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-              lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
+              lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
               lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
               lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
               ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
                   lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
-                  lemma5 = cong (λ k → od→ord (A ∩ k )) Ord-ord
+                  lemma5 = cong (λ k → od→ord (A ∩ k )) {!!}
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where
 
@@ -517,7 +481,7 @@
                    def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) ))) ( osuc y )
                 ≡⟨⟩
                    osuc y o<  omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) )
-                ≡⟨ cong (λ k → osuc y o<  omax (od→ord x) k ) (sym ord-Ord)  ⟩
+                ≡⟨ cong (λ k → osuc y o<  omax (od→ord x) k ) {!!}  ⟩
                    osuc y o<  omax (od→ord x) (omax (od→ord x)  (od→ord x)  ) 
                 ≡⟨ cong (λ k → osuc y o<  k ) (omxxx  (od→ord x) )  ⟩
                    osuc y o< osuc (osuc (od→ord x))
@@ -525,13 +489,13 @@
          infinite : OD {suc n}
          infinite = Ord omega 
          infinity∅ : Ord omega  ∋ od∅ {suc n}
-         infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl
+         infinity∅ = o<-subst (case1 (s≤s z≤n) ) {!!} refl
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
               eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
               eq = let open ≡-Reasoning in begin
                     osuc (od→ord x)
-                 ≡⟨ ord-Ord  ⟩
+                 ≡⟨ {!!}  ⟩
                     od→ord (Ord (osuc (od→ord x)))
                  ≡⟨ cong ( λ k → od→ord  k ) ( sym (==→o≡ ( ⇔→==  uxxx-ord ))) ⟩
                     od→ord (Union (x , (x , x)))
diff -r 2eafa89733ed -r c848550c8b39 ordinal.agda
--- a/ordinal.agda	Mon Jul 08 18:26:33 2019 +0900
+++ b/ordinal.agda	Mon Jul 08 19:35:23 2019 +0900
@@ -118,6 +118,14 @@
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
 
+case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
+case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
+... | refl = nat-≡< refl lt1
+
+case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
+case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
+... | refl = nat-≡< refl lt1
+
 o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy  → ox o< oy  → ⊥
 o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt