# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562508167 -32400
# Node ID 312e27aa3cb5516825e1550696aa3d6bc59a4908
# Parent  53077af367e90a024d30243b82eda6e2641cb9e1
remove otrans again. start over

diff -r 53077af367e9 -r 312e27aa3cb5 HOD.agda
--- a/HOD.agda	Sun Jul 07 22:23:02 2019 +0900
+++ b/HOD.agda	Sun Jul 07 23:02:47 2019 +0900
@@ -16,7 +16,6 @@
 record HOD {n : Level}  : Set (suc n) where
   field
     def : (x : Ordinal {n} ) → Set n
-    otrans : {x : Ordinal {n} } → def x → { y : Ordinal {n} } → y o< x → def y
 
 open HOD
 open import Data.Unit
@@ -49,9 +48,7 @@
 
 -- Ordinal in HOD ( and ZFSet )
 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
-Ord {n} a = record { def = λ y → y o< a ; otrans = lemma }  where
-   lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
-   lemma {x}  x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
+Ord {n} a = record { def = λ y → y o< a }  
 
 od∅ : {n : Level} → HOD {n} 
 od∅ {n} = Ord o∅ 
@@ -94,9 +91,7 @@
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
 cseq : {n : Level} →  HOD {n} →  HOD {n}
-cseq x = record { def = λ y → def x (osuc y) ; otrans = lemma } where
-   lemma : {ox : Ordinal} → def x (osuc ox) → { oy : Ordinal}→ oy o< ox → def x (osuc oy)
-   lemma {ox}  oox<Ox {oy} oy<ox  = otrans x  oox<Ox (osucc oy<ox )
+cseq x = record { def = λ y → def x (osuc y) } where
 
 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -145,10 +140,6 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
 
-transitive : {n : Level } { z y x : HOD {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 ) 
-... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y ) 
-
 ∅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 Φ<
@@ -206,7 +197,7 @@
 o≡→¬c< : {n : Level} →  { x y : HOD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡  (orefl oeq ) (c<→o< lt) 
 
-∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ ; otrans = λ () } == od∅ {n} 
+∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} (case1 ())
 eq← ∅0 {w} (case2 ())
@@ -236,9 +227,7 @@
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y ; otrans = lemma }   where
-  lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y
-  lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z }
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
 
 Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
@@ -296,12 +285,7 @@
     ; isZF = isZF 
  } where
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
-       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
-            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
-       lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
-           y<X : X ∋ ord→od y
-           y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
+    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧  ( x == ψ (Ord y)  ))))
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
@@ -369,8 +353,7 @@
          ... | 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 (Ord a) (proj1 (lemma1 lt) )
-                   (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where
+         ... | case2 lt = {!!} where
               sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
               minsup :  HOD
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
@@ -427,7 +410,7 @@
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
          union→ X z u xx | tri< a ¬b ¬c | ()
          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 = otrans X (proj1 xx) c
+         union→ X z u xx | tri> ¬a ¬b c = {!!}
          union← :  (X z : HOD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
              lemma : X ∋ union-u {X} {z} X∋z
@@ -435,35 +418,12 @@
 
          -- ψ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)
-         selection {X} {ψ} {y} =  record { proj1 = λ s → record {
-             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
-         -- ψ< :  {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} →  ψ y ∋ x → ψ y' == x 
-         -- ψ< = {!!}
+         selection : {ψ : HOD → Set (suc n)} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection {X} {ψ} {y} = {!!}
          replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 = lemma 
-                ; proj2 = sup-o∋ψx
-             }
-            where
-             sup-o∋ψx : Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od (od→ord (ψ x))
-             sup-o∋ψx = def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))} { od→ord (ord→od (od→ord (ψ x)))}
-                    (sup-c< ψ {x}) refl (sym diso)
-             lemma  : (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y →
-                      ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁)))
-             lemma y lt1 not = not (minα (od→ord x) (sup-x ( λ w → od→ord (ψ (ord→od w ))))) (record {
-                      proj1 = ?
-                    ; proj2 = subst₂ (λ k j → k == j ) refl oiso (o≡→== {!!}) } ) where
-                 lemma1 : y o< osuc ( od→ord (ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w ))) )))) 
-                 lemma1 = o<-subst (sup-lb lt1) diso refl
-                 lemma2 : ord→od y ≡ ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w )))))
-                 lemma2 with osuc-≡< lemma1
-                 lemma2 | case1 refl = subst (λ k → ord→od y ≡ k ) oiso  refl
-                 lemma2 | case2 t = {!!}
+         replacement← {ψ} X x lt = {!!}
          replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where
+         replacement→ {ψ} X x lt = contra-position lemma {!!} where
             lemma :  ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
             lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 ))
 
@@ -476,7 +436,7 @@
              lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
              lemma1 {x₁} s = ⊥-elim  ( minimul-1 x not (ord→od x₁) lemma3 ) where
                  lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
-                 lemma3 = proj1 s x₁ (proj2 s)
+                 lemma3 = {!!}
              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) ))
 
diff -r 53077af367e9 -r 312e27aa3cb5 ordinal-definable.agda
--- a/ordinal-definable.agda	Sun Jul 07 22:23:02 2019 +0900
+++ b/ordinal-definable.agda	Sun Jul 07 23:02:47 2019 +0900
@@ -311,7 +311,7 @@
     ; isZF = isZF 
  } where
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
-    Select X ψ = record { def = λ x →  ((y : Ordinal {suc n}) → def X y → ψ ( ord→od y )) ∧ def X x  } 
+    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) } 
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
     _∩_ : ( A B : OD {suc n} ) → OD
@@ -348,7 +348,7 @@
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
-       ;   selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} 
+       ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
        ;   replacement← = replacement←
        ;   replacement→ = replacement→
      } where
@@ -408,19 +408,17 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (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
-         selection : {ψ : OD → Set (suc n)} {X y : OD} →  (((y : OD) → X ∋ y → ψ y) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
+         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
          selection {ψ} {X} {y} = record {
-              proj1 = λ cond → record { proj1 = λ y X>y → proj1 cond (ord→od y) (subst (λ k → def X k ) (sym diso) X>y) ; proj2 = proj2 cond }
-            ; proj2 = λ select → record { proj1 = λ y X>y → subst (λ k → ψ k ) oiso (proj1 select (od→ord y) X>y )  ; proj2 =  proj2 select } 
-           } where
-               lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y
-               lemma cond = (proj1 cond) y (proj2 cond)
+              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
+           }
          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)} ) )
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) )
+         replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!}) )
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
@@ -433,7 +431,7 @@
             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 with proj1 t y (proj2 t)
+            reg {y} t with {!!}
             ... | x∈∅ = o<-subst (proj1 x∈∅) diso 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  
diff -r 53077af367e9 -r 312e27aa3cb5 zf.agda
--- a/zf.agda	Sun Jul 07 22:23:02 2019 +0900
+++ b/zf.agda	Sun Jul 07 23:02:47 2019 +0900
@@ -75,7 +75,7 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (y ∈  Select X ψ ) 
+     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ 
      replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )