Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff BAlgbra.agda @ 329:5544f4921a44
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 12:32:09 +0900 |
parents | d9d3654baee1 |
children | 12071f79f3cf |
line wrap: on
line diff
--- a/BAlgbra.agda Sun Jul 05 11:40:55 2020 +0900 +++ b/BAlgbra.agda Sun Jul 05 12:32:09 2020 +0900 @@ -24,16 +24,16 @@ open _∨_ open Bool -_∩_ : ( A B : OD ) → OD +_∩_ : ( A B : HOD ) → HOD A ∩ B = record { def = λ x → def A x ∧ def B x } -_∪_ : ( A B : OD ) → OD +_∪_ : ( A B : HOD ) → HOD A ∪ B = record { def = λ x → def A x ∨ def B x } -_\_ : ( A B : OD ) → OD +_\_ : ( A B : HOD ) → HOD A \ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } -∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) +∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x lemma1 {x} lt = lemma3 lt where @@ -49,7 +49,7 @@ lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) -∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) +∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } @@ -57,7 +57,7 @@ lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } -dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) +dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x lemma1 {x} lt with proj2 lt @@ -67,7 +67,7 @@ lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } -dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) +dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }