Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 247:d09437fcfc7c
fix pair
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Aug 2019 12:27:20 +0900 |
| parents | 846e0926bb89 |
| children | 2ea2a19f9cd6 |
line wrap: on
line diff
--- a/OD.agda Mon Aug 26 02:50:16 2019 +0900 +++ b/OD.agda Mon Aug 26 12:27:20 2019 +0900 @@ -269,7 +269,7 @@ 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 = Ord (omax (od→ord x) (od→ord y)) + 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 @@ -294,7 +294,8 @@ isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite isZF = record { isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } - ; pair = pair + ; pair→ = pair→ + ; pair← = pair← ; union→ = union→ ; union← = union← ; empty = empty @@ -311,9 +312,17 @@ ; choice = choice } where - pair : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) - proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) - proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) + pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) + pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) + + pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t + pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) + pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) + + -- pair0 : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) + -- proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) + -- proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) empty : (x : OD ) → ¬ (od∅ ∋ x) empty x = ¬x<0