Members/kono/Proof/ZF-in-agda: constructible-set.agda comparison

comparison constructible-set.agda @ 23:7293a151d949

Sup

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 18 May 2019 08:29:08 +0900
parents	3da2c00bd24d
children	3186bbee99dd

comparison

equal deleted inserted replaced

-:3da2c00bd24d
+:7293a151d949
 open import Level
 module constructible-set (n : Level) where
 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
 data OrdinalD  : (lv : Nat) → Set n where
 Φ : {lv : Nat} → OrdinalD  lv
 maxα x y with <-cmp (lv x) (lv y)
 maxα x y | tri< a ¬b ¬c = x
 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
 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
 OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
 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
 ; trans         = OrdTrans
 }
 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
 ( 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
 field
 α : Ordinal
 constructible : Ordinal  → Set (suc n)
 open ConstructibleSet
 _∋_  : (ConstructibleSet ) → (ConstructibleSet  ) → Set (suc n)
-a ∋ x  =  ((α a ≡ α x)  ∨ ( α x o< α a ))
+a ∋ x  = ( α x o< α a ) ∧ constructible a ( α x )
-∧ 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 = {!!}
 ; Select = Select
 ; Replace = Replace
 conv ψ x with ψ x
 ... | t =  Lift ( suc n ) ⊤
 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
 Union a = {!!}

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison constructible-set.agda @ 23:7293a151d949