### diff constructible-set.agda @ 23:7293a151d949

Sup
author Shinji KONO Sat, 18 May 2019 08:29:08 +0900 3da2c00bd24d 3186bbee99dd
line wrap: on
line diff
```--- 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```