Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/BAlgebra.agda @ 1150:fe0129c40745

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Jan 2023 11:21:18 +0900
parents d122d0c1b094
children 8a071bf52407
comparison
equal deleted inserted replaced
1149:f8a30e568eca 1150:fe0129c40745
30 open HOD 30 open HOD
31 31
32 open _∧_ 32 open _∧_
33 open _∨_ 33 open _∨_
34 open Bool 34 open Bool
35
36 --_∩_ : ( A B : HOD ) → HOD
37 --A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
38 -- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
39
40 ∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
41 ∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
42
43 _∪_ : ( A B : HOD ) → HOD
44 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
45 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
46 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
47 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
48 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
49
50 _＼_ : ( A B : HOD ) → HOD
51 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
52
53 ¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
54 ¬∅∋ {x} = ¬x<0
55 35
56 L＼L=0 : { L : HOD } → L ＼ L ≡ od∅ 36 L＼L=0 : { L : HOD } → L ＼ L ≡ od∅
57 L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← = lem1 } ) where 37 L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← = lem1 } ) where
58 lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x 38 lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
59 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx) 39 lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)