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

comparison constructible-set.agda @ 20:31626f36cd94

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 16:08:34 +0900
parents 47995eb521d4
children 6d9fdd1dfa79
comparison
equal deleted inserted replaced
19:47995eb521d4 20:31626f36cd94
127 α : Ordinal 127 α : Ordinal
128 constructible : Ordinal → Set (suc 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 (suc n)
133 a ∋ x = (α a ≡ α x) ∨ ( α x o< α a ) 133 a ∋ x = ((α a ≡ α x) ∨ ( α x o< α a ))
134 ∧ constructible a ( α x )
135
134 136
135 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c 137 -- 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 138 -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
137 -- ... | t1 | t2 = {!!} 139 -- ... | t1 | t2 = {!!}
140
141 open import Data.Unit
138 142
139 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)} 143 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)}
140 ConstructibleSet→ZF = record { 144 ConstructibleSet→ZF = record {
141 ZFSet = ConstructibleSet 145 ZFSet = ConstructibleSet
142 ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b ) 146 ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b )
143 ; _≈_ = _≡_ 147 ; _≈_ = _≡_
144 ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ } 148 ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ }
145 ; _,_ = _,_ 149 ; _,_ = _,_
146 ; Union = Union 150 ; Union = Union
147 ; Power = {!!} 151 ; Power = {!!}
148 ; Select = {!!} 152 ; Select = Select
149 ; Replace = {!!} 153 ; Replace = Replace
150 ; infinite = {!!} 154 ; infinite = {!!}
151 ; isZF = {!!} 155 ; isZF = {!!}
152 } where 156 } where
153 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet 157 conv : (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet → Set (suc n)
154 Select X ψ = record { α = α X ; constructible = λ x → ( ψ (record { α = x ; constructible = λ x → constructible X x } ) ) } 158 conv ψ x with ψ x
159 ... | t = Lift ( suc n ) ⊤
160 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet
161 Select X ψ = record { α = α X ; constructible = λ x → (conv ψ) (record { α = x ; constructible = λ x → constructible X x } ) }
162 Replace : (X : ConstructibleSet) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
163 Replace X ψ = record { α = α X ; constructible = λ x → {!!} }
155 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet 164 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
156 a , b = Select {!!} {!!} 165 a , b = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} }
157 Union : ConstructibleSet → ConstructibleSet 166 Union : ConstructibleSet → ConstructibleSet
158 Union a = {!!} 167 Union a = {!!}