# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563678590 -32400
# Node ID 7012158bf2d9c6cc6e745175bbad317957e4ac86
# Parent  11490a3170d4005292b01af651733614892c5393
 ...

diff -r 11490a3170d4 -r 7012158bf2d9 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jul 20 14:05:32 2019 +0900
+++ b/ordinal-definable.agda	Sun Jul 21 12:09:50 2019 +0900
@@ -25,11 +25,17 @@
 
 
 postulate      
+  od=ord : {n : Level } → { x : Ordinal {n}} → ord→od x ≡ Ord x
   -- a property of supermum required in Power Set Axiom
   sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
-  o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
+
+o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
+o<→c< {n} {x} {y} lt  = def-subst {n} {_} {_} {ord→od y} {x} lt (sym od=ord) refl
+
+ord=od : {n : Level } → { x : OD {n}} → x ≡ Ord (od→ord x)
+ord=od {n} {x} = subst ( λ k → k ≡ Ord (od→ord x) ) oiso od=ord 
 
 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
 transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y ) 
@@ -201,7 +207,7 @@
               minsup :  OD
               minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
               lemma-t : csuc minsup ∋ t
-              lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 
+              lemma-t = def-subst (o<→c< (o<-subst (sup-lb (o<-subst (c<→o< {!!}) refl diso )) refl refl ) ) {!!} {!!}
               lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
               lemma-s with osuc-≡< ( o<-subst (c<→o< {!!}  ) refl diso  )
               lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl
@@ -212,7 +218,7 @@
          -- 
          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 refl lemma1 where
               lemma-eq :  ZFSubset A t == t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
@@ -223,7 +229,7 @@
               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 = {!!} where -- lemma <-osuc where
+         union-lemma-u {X} {z} U>z = def-subst (lemma <-osuc ) od=ord refl 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} (o<→c< lt) refl refl
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
@@ -236,7 +242,7 @@
          union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
          union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z ))) -- (X ∋ csuc z) ∧ (csuc z ∋ z )
          union← X z X∋z not = not (csuc z) 
-             record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym {!!}) ; proj2 = union-lemma-u X∋z } 
+             record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (trans (sym diso) {!!} ) ; proj2 = union-lemma-u X∋z } 
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
@@ -251,7 +257,7 @@
              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)} ) )
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (def-subst (proj2 lt) {!!} refl )) where
             lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
                     → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
             lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
@@ -264,13 +270,13 @@
          minimul-o x  not = od∅   
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-         proj1 (regularity x not ) = {!!}
+         proj1 (regularity x not ) = def-subst (¬∅=→∅∈ not) {!!} refl
          proj2 (regularity x not ) = record { eq→ = reg ; eq← = lemma } where
             lemma : {ox : Ordinal} → def od∅ ox → def (Select (minimul x not) (λ y → (minimul x not ∋ y) ∧ (x ∋ y))) ox
             lemma (case1 ())
             lemma (case2 ())
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
-            reg {y} t = ⊥-elim ( ¬x<0 {!!} )
+            reg {y} t = ⊥-elim ( ¬x<0 (def-subst (proj1 (proj2 t )) {!!} refl ))
 
          extensionality : {A B : OD {suc n}} → ((z : OD) → (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