comparison OD.agda @ 254:2ea2a19f9cd6

ordered pair clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:16:51 +0900
parents d09437fcfc7c
children 53b7acd63481
comparison
equal deleted inserted replaced
253:0446b6c5e7bc 254:2ea2a19f9cd6
169 is-o∅ x with trio< x o∅ 169 is-o∅ x with trio< x o∅
170 is-o∅ x | tri< a ¬b ¬c = no ¬b 170 is-o∅ x | tri< a ¬b ¬c = no ¬b
171 is-o∅ x | tri≈ ¬a b ¬c = yes b 171 is-o∅ x | tri≈ ¬a b ¬c = yes b
172 is-o∅ x | tri> ¬a ¬b c = no ¬b 172 is-o∅ x | tri> ¬a ¬b c = no ¬b
173 173
174 _,_ : OD → OD → OD
175 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y))
176 <_,_> : (x y : OD) → OD
177 < x , y > = (x , x ) , (x , y )
178
179 exg-pair : { x y : OD } → (x , y ) == ( y , x )
180 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
181 left : {z : Ordinal} → def (x , y) z → def (y , x) z
182 left (case1 t) = case2 t
183 left (case2 t) = case1 t
184 right : {z : Ordinal} → def (y , x) z → def (x , y) z
185 right (case1 t) = case2 t
186 right (case2 t) = case1 t
187
188 ==-trans : { x y z : OD } → x == y → y == z → x == z
189 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) }
190
191 ==-sym : { x y : OD } → x == y → y == x
192 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t }
193
194 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
195 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
196
197 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
198 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
199
200 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
201 eq-prod refl refl = refl
202
203 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
204 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
205 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
206 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y)
207 lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl)
208 lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
209 lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
210 lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
211 lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl)
212 lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
213 lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
214 lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
215 lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where
216 lemma3 : ( x , x ) == ( y , z )
217 lemma3 = ==-trans eq exg-pair
218 lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
219 lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
220 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
221 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
222 lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
223 lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
224 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
225 ... | refl with lemma2 (==-sym eq )
226 ... | refl = refl
227 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
228 lemmax : x ≡ x'
229 lemmax with eq→ eq {od→ord (x , x)} (case1 refl)
230 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x')
231 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
232 ... | refl = lemma1 (ord→== s )
233 lemmay : y ≡ y'
234 lemmay with lemmax
235 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
236 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 ))
237
174 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p 238 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
175 ppp {p} {a} d = d 239 ppp {p} {a} d = d
176 240
177 -- 241 --
178 -- Axiom of choice in intutionistic logic implies the exclude middle 242 -- Axiom of choice in intutionistic logic implies the exclude middle
266 ZFSet = OD 330 ZFSet = OD
267 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 331 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
268 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 332 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
269 Replace : OD → (OD → OD ) → OD 333 Replace : OD → (OD → OD ) → OD
270 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 334 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
271 _,_ : OD → OD → OD
272 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y))
273 _∩_ : ( A B : ZFSet ) → ZFSet 335 _∩_ : ( A B : ZFSet ) → ZFSet
274 A ∩ B = record { def = λ x → def A x ∧ def B x } 336 A ∩ B = record { def = λ x → def A x ∧ def B x }
275 Union : OD → OD 337 Union : OD → OD
276 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 338 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
277 _∈_ : ( A B : ZFSet ) → Set n 339 _∈_ : ( A B : ZFSet ) → Set n
531 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 593 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
532 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 594 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
533 } 595 }
534 596
535 597
536 _,_ = ZF._,_ OD→ZF
537 Union = ZF.Union OD→ZF 598 Union = ZF.Union OD→ZF
538 Power = ZF.Power OD→ZF 599 Power = ZF.Power OD→ZF
539 Select = ZF.Select OD→ZF 600 Select = ZF.Select OD→ZF
540 Replace = ZF.Replace OD→ZF 601 Replace = ZF.Replace OD→ZF
541 isZF = ZF.isZF OD→ZF 602 isZF = ZF.isZF OD→ZF