Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff BAlgbra.agda @ 376:6c72bee25653
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 20 Jul 2020 16:28:12 +0900 |
parents | 17adeeee0c2a |
children | 8c092c042093 |
line wrap: on
line diff
--- a/BAlgbra.agda Mon Jul 20 16:22:44 2020 +0900 +++ b/BAlgbra.agda Mon Jul 20 16:28:12 2020 +0900 @@ -1,4 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Ordinals module BAlgbra {n : Level } (O : Ordinals {n}) where @@ -56,13 +55,13 @@ lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x})) -∩-Select : { A B : HOD } → 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} → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x - lemma1 {x} lt = record { proj1 = proj1 {!!} ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 {!!} )) } - lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x - lemma2 {x} lt = {!!} -- record { proj1 = proj1 lt ; proj2 = - -- record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } + lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x + lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) } + lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x + lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = + record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } 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