# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558135748 -32400
# Node ID 7293a151d94910583723995aefb9cb5177cc9ae7
# Parent  3da2c00bd24df0148c26ca2e086262ed4110ff9c
Sup

diff -r 3da2c00bd24d -r 7293a151d949 constructible-set.agda
--- a/constructible-set.agda	Thu May 16 17:20:45 2019 +0900
+++ b/constructible-set.agda	Sat May 18 08:29:08 2019 +0900
@@ -3,7 +3,7 @@
 
 open import zf
 
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
 open import  Relation.Binary.PropositionalEquality
 
@@ -101,7 +101,19 @@
 maxα x y | tri> ¬a ¬b c = y
 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
 
-OrdTrans : Transitive (λ ( a b : Ordinal ) → (a ≡ b) ∨ (Ordinal.lv a < Ordinal.lv b) ∨ (Ordinal.ord a d< Ordinal.ord b) )
+_o≤_ : Ordinal → Ordinal → Set n
+a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+
+trio< : Trichotomous  _≡_  _o<_ 
+trio< a b with <-cmp (lv a) (lv b)
+trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) {!!}
+trio< a b | tri> ¬a ¬b c = tri> {!!} (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c)
+trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b {!!} )  {!!}
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ {!!} refl {!!}
+trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> {!!} {!!} (case2 c)
+
+OrdTrans : Transitive _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
@@ -116,7 +128,7 @@
 OrdPreorder : Preorder n n n
 OrdPreorder = record { Carrier = Ordinal
    ; _≈_  = _≡_ 
-   ; _∼_   = λ a b → (a ≡ b)  ∨ ( a o< b )  
+   ; _∼_   = _o≤_
    ; isPreorder   = record {
         isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
         ; reflexive     = case1 
@@ -134,17 +146,6 @@
     ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
 
-record SupR (ψ : Ordinal → Ordinal ) : Set n where
-  field
-    sup : Ordinal
-    smax : { x : Ordinal } → ψ x o< sup
-
-open SupR
-
-Sup : (ψ : Ordinal → Ordinal )  → SupR ψ
-sup (Sup ψ) = {!!}
-smax (Sup ψ) = {!!}
-     
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
 record ConstructibleSet  : Set (suc (suc n)) where
@@ -155,22 +156,44 @@
 open ConstructibleSet
 
 _∋_  : (ConstructibleSet ) → (ConstructibleSet  ) → Set (suc n)
-a ∋ x  =  ((α a ≡ α x)  ∨ ( α x o< α a ))
-    ∧ constructible a ( α x )
-    
+a ∋ x  = ( α x o< α a ) ∧ constructible a ( α x )
+
+c∅ : ConstructibleSet
+c∅  = record {α = o∅ ; constructible = λ x → Lift (suc n) ⊥ }
+
+record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m  ) (ψ : S → S ) (X : S) : Set (n ⊔ m)  where
+  field
+    sup : S
+    smax  : ∀ { x : S } → x ≤ X  → ψ x ≤ sup 
+    suniq : {max : S} → ( ∀ { x :  S } → x ≤ X  → ψ x ≤ max ) → max ≤ sup 
+
+open SupR
+
+_⊆_ : ( A B : ConstructibleSet  ) → ∀{ x : ConstructibleSet } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+suptraverse : (X : ConstructibleSet ) ( max : ConstructibleSet) ( ψ : ConstructibleSet  → ConstructibleSet ) → ConstructibleSet
+suptraverse X max ψ  = {!!} 
+
+Sup : (ψ : ConstructibleSet → ConstructibleSet )  → (X : ConstructibleSet)  → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
+sup (Sup ψ X ) = suptraverse X c∅ ψ 
+smax (Sup ψ X ) = {!!} -- TransFinite {!!} {!!} {!!} {!!} {!!} 
+suniq (Sup ψ X ) = {!!}
+     
 
 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
 -- transitiveness  a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
 -- ... | t1 | t2 = {!!}
 
 open import Data.Unit
+open SupR
 
 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)}
 ConstructibleSet→ZF   = record { 
     ZFSet = ConstructibleSet 
     ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b )
     ; _≈_ = _≡_ 
-    ; ∅  = record {α = o∅ ; constructible = λ x → Lift (suc n) ⊥ }
+    ; ∅  = c∅ 
     ; _,_ = _,_
     ; Union = Union
     ; Power = {!!}
@@ -185,7 +208,7 @@
     Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet
     Select X ψ = record { α = α X ; constructible = λ x → (conv ψ) (record { α = x ; constructible = λ x → constructible X x }  ) }
     Replace : (X : ConstructibleSet) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
-    Replace X ψ  = record { α = α X ; constructible = λ x →  {!!}  }
+    Replace X ψ  = record { α = α (sup (Sup ψ X))  ; constructible = λ x → {!!}  }
     _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
     a , b  = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} }
     Union : ConstructibleSet → ConstructibleSet
diff -r 3da2c00bd24d -r 7293a151d949 zf.agda
--- a/zf.agda	Thu May 16 17:20:45 2019 +0900
+++ b/zf.agda	Sat May 18 08:29:08 2019 +0900
@@ -2,6 +2,9 @@
 
 open import Level
 
+data Bool : Set where
+   true : Bool
+   false : Bool
 
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
    field 
@@ -60,8 +63,8 @@
      union← : ( X x y : ZFSet  ) → Union X  ∋ y → X ∋ x  → x ∋ y 
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
-  _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
-  _⊆_ A B {x} {A∋x} = B ∋ x
+  _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
+  _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
@@ -72,8 +75,8 @@
   field
      empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
      -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
-     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x} {y} →  _⊆_ t A {x} {y}
-     power← : ∀( A t : ZFSet  ) → ∀ {x} {y} →  _⊆_ t A {x} {y} → Power A ∋ t 
+     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  _⊆_ t A {x} 
+     power← : ∀( A t : ZFSet  ) → ∀ {x}  →  _⊆_ t A {x}  → Power A ∋ t 
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )