Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/OD.agda Thu Aug 29 16:08:46 2019 +0900 +++ b/OD.agda Thu Aug 29 16:16:51 2019 +0900 @@ -171,6 +171,70 @@ is-o∅ x | tri≈ ¬a b ¬c = yes b is-o∅ x | tri> ¬a ¬b c = no ¬b +_,_ : OD → OD → OD +x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) +<_,_> : (x y : OD) → OD +< x , y > = (x , x ) , (x , y ) + +exg-pair : { x y : OD } → (x , y ) == ( y , x ) +exg-pair {x} {y} = record { eq→ = left ; eq← = right } where + left : {z : Ordinal} → def (x , y) z → def (y , x) z + left (case1 t) = case2 t + left (case2 t) = case1 t + right : {z : Ordinal} → def (y , x) z → def (x , y) z + right (case1 t) = case2 t + right (case2 t) = case1 t + +==-trans : { x y z : OD } → x == y → y == z → x == z +==-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) } + +==-sym : { x y : OD } → x == y → y == x +==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } + +ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y +ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) + +od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y +od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) + +eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > +eq-prod refl refl = refl + +prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) +prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where + lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y + lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) + lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b + lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) + lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y + lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where + lemma3 : ( x , x ) == ( y , z ) + lemma3 = ==-trans eq exg-pair + lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y + lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) + lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) + lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) + lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z + lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) + lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z + ... | refl with lemma2 (==-sym eq ) + ... | refl = refl + lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z + lemmax : x ≡ x' + lemmax with eq→ eq {od→ord (x , x)} (case1 refl) + lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') + lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' + ... | refl = lemma1 (ord→== s ) + lemmay : y ≡ y' + lemmay with lemmax + ... | refl with lemma4 eq -- with (x,y)≡(x,y') + ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) + ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p ppp {p} {a} d = d @@ -268,8 +332,6 @@ Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD → (OD → OD ) → OD Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } - _,_ : OD → OD → OD - x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = record { def = λ x → def A x ∧ def B x } Union : OD → OD @@ -533,7 +595,6 @@ } -_,_ = ZF._,_ OD→ZF Union = ZF.Union OD→ZF Power = ZF.Power OD→ZF Select = ZF.Select OD→ZF