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

comparison constructible-set.agda @ 18:627a79e61116

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 May 2019 10:55:34 +0900
parents 6a668c6086a5
children 47995eb521d4
comparison
equal deleted inserted replaced
17:6a668c6086a5 18:627a79e61116
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 data Constructible ( α : Ordinal ) : Set (suc n) where
126 fsub : ( ψ : Ordinal → Set n ) → Constructible α
127 xself : Ordinal → Constructible α
128
129 record ConstructibleSet : Set (suc n) where 125 record ConstructibleSet : Set (suc n) where
130 field 126 field
131 α : Ordinal 127 α : Ordinal
132 constructible : Constructible α 128 constructible : Ordinal → Set n
133 129
134 open ConstructibleSet 130 open ConstructibleSet
135 131
136 data _c∋_ : {α α' : Ordinal } → 132 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
137 Constructible α → Constructible α' → Set n where 133 a ∋ x = (α a ≡ α x) ∨ ( α x o< α a )
138 c> : {α α' : Ordinal }
139 (ta : Constructible α ) ( tx : Constructible α' ) → α' o< α → ta c∋ tx
140 xself-fsub : {α : Ordinal }
141 (ta : Ordinal ) ( ψ : Ordinal → Set n ) → _c∋_ {α} {α} (xself ta ) ( fsub ψ)
142 fsub-fsub : {α : Ordinal }
143 ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n ) →
144 ( ∀ ( x : Ordinal ) → ψ x → ψ₁ x ) → _c∋_ {α} {α} ( fsub ψ ) ( fsub ψ₁)
145
146 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
147 a ∋ x = constructible a c∋ constructible x
148 134
149 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c 135 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
150 -- 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
151 -- ... | t1 | t2 = {!!} 137 -- ... | t1 | t2 = {!!}
152 138
153 data _c≈_ : {α α' : Ordinal} → 139 ConstructibleSet→ZF : ZF {suc n} {suc n}
154 Constructible α → Constructible α' → Set n where
155 crefl : {α : Ordinal } → _c≈_ {α} {α} (xself α ) (xself α )
156 feq : {lv : Nat} {α : Ordinal }
157 → ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n )
158 → (∀ ( x : Ordinal ) → ψ x ⇔ ψ₁ x ) → _c≈_ {α} {α} ( fsub ψ ) ( fsub ψ₁)
159
160 _≈_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
161 a ≈ x = constructible a c≈ constructible x
162
163 ConstructibleSet→ZF : ZF {suc n}
164 ConstructibleSet→ZF = record { 140 ConstructibleSet→ZF = record {
165 ZFSet = ConstructibleSet 141 ZFSet = ConstructibleSet
166 ; _∋_ = _∋_ 142 ; _∋_ = λ a b → Lift (suc n) ( a ∋ b )
167 ; _≈_ = _≈_ 143 ; _≈_ = _≡_
168 ; ∅ = record { α = record {lv = Zero ; ord = Φ } ; constructible = xself ( record {lv = Zero ; ord = Φ }) } 144 ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift n ⊥ }
169 ; _×_ = {!!} 145 ; _,_ = _,_
170 ; Union = {!!} 146 ; Union = Union
171 ; Power = {!!} 147 ; Power = {!!}
172 ; Select = {!!} 148 ; Select = Select
173 ; Replace = {!!} 149 ; Replace = {!!}
174 ; infinite = {!!} 150 ; infinite = {!!}
175 ; isZF = {!!} 151 ; isZF = {!!}
176 } 152 } where
153 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet
154 Select = {!!}
155 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
156 a , b = Select {!!} {!!}
157 Union : ConstructibleSet → ConstructibleSet
158 Union a = {!!}