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

comparison src/ODC.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents 105f8d6c51fb
children e086a266c6b7
comparison
equal deleted inserted replaced
1095:08b6aa6870d9 1096:55ab5de1ae02
93 or-exclude {A} {B} (case1 a) | case1 a0 = case1 a 93 or-exclude {A} {B} (case1 a) | case1 a0 = case1 a
94 or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a ) 94 or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a )
95 or-exclude {A} {B} (case2 b) | case1 a = case1 a 95 or-exclude {A} {B} (case2 b) | case1 a = case1 a
96 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫ 96 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
97 97
98 open _⊆_
99
100 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 98 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
101 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where 99 power→⊆ A t PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
102 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
103 t1 = power→ A t PA∋t
104 100
105 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y ) 101 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
106 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where 102 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where
107 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z 103 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z
108 p01 {z} xyz = double-neg-eilm ( power→ A x ax (proj1 xyz )) 104 p01 {z} xyz = power→ A x ax (proj1 xyz )
109 105
110 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) 106 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
111 OrdP x y with trio< x (& y) 107 OrdP x y with trio< x (& y)
112 OrdP x y | tri< a ¬b ¬c = no ¬c 108 OrdP x y | tri< a ¬b ¬c = no ¬c
113 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 109 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )