Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
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