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

comparison constructible-set.agda @ 19:47995eb521d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 May 2019 11:40:18 +0900
parents 627a79e61116
children 31626f36cd94
comparison
equal deleted inserted replaced
18:627a79e61116 19:47995eb521d4
120 } 120 }
121 } 121 }
122 122
123 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' 123 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
124 124
125 record ConstructibleSet : Set (suc n) where 125 record ConstructibleSet : Set (suc (suc n)) where
126 field 126 field
127 α : Ordinal 127 α : Ordinal
128 constructible : Ordinal → Set n 128 constructible : Ordinal → Set (suc n)
129 129
130 open ConstructibleSet 130 open ConstructibleSet
131 131
132 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n 132 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
133 a ∋ x = (α a ≡ α x) ∨ ( α x o< α a ) 133 a ∋ x = (α a ≡ α x) ∨ ( α x o< α a )
134 134
135 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c 135 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
136 -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c 136 -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
137 -- ... | t1 | t2 = {!!} 137 -- ... | t1 | t2 = {!!}
138 138
139 ConstructibleSet→ZF : ZF {suc n} {suc n} 139 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)}
140 ConstructibleSet→ZF = record { 140 ConstructibleSet→ZF = record {
141 ZFSet = ConstructibleSet 141 ZFSet = ConstructibleSet
142 ; _∋_ = λ a b → Lift (suc n) ( a ∋ b ) 142 ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b )
143 ; _≈_ = _≡_ 143 ; _≈_ = _≡_
144 ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift n ⊥ } 144 ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ }
145 ; _,_ = _,_ 145 ; _,_ = _,_
146 ; Union = Union 146 ; Union = Union
147 ; Power = {!!} 147 ; Power = {!!}
148 ; Select = Select 148 ; Select = {!!}
149 ; Replace = {!!} 149 ; Replace = {!!}
150 ; infinite = {!!} 150 ; infinite = {!!}
151 ; isZF = {!!} 151 ; isZF = {!!}
152 } where 152 } where
153 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet 153 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet
154 Select = {!!} 154 Select X ψ = record { α = α X ; constructible = λ x → ( ψ (record { α = x ; constructible = λ x → constructible X x } ) ) }
155 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet 155 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
156 a , b = Select {!!} {!!} 156 a , b = Select {!!} {!!}
157 Union : ConstructibleSet → ConstructibleSet 157 Union : ConstructibleSet → ConstructibleSet
158 Union a = {!!} 158 Union a = {!!}