Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/PFOD.agda @ 1100:c90eec304cfa
PFOD
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Dec 2022 14:00:57 +0900 |
parents | c2501d308c95 |
children | d122d0c1b094 |
comparison
equal
deleted
inserted
replaced
1099:c2501d308c95 | 1100:c90eec304cfa |
---|---|
136 le00 = subst (λ k → odef X k) &iso ( ω→2f≡i1 _ _ ωx1 lt (iso ωx1) ) | 136 le00 = subst (λ k → odef X k) &iso ( ω→2f≡i1 _ _ ωx1 lt (iso ωx1) ) |
137 eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef infinite k) &iso le02 , ⟪ le02 , le01 ⟫ ⟫ where | 137 eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef infinite k) &iso le02 , ⟪ le02 , le01 ⟫ ⟫ where |
138 le02 : infinite ∋ * x | 138 le02 : infinite ∋ * x |
139 le02 = power→ infinite _ lt (subst (λ k → odef X k) (sym &iso) Xx) | 139 le02 = power→ infinite _ lt (subst (λ k → odef X k) (sym &iso) Xx) |
140 le01 : (wx : odef infinite (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1 | 140 le01 : (wx : odef infinite (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1 |
141 le01 wx = ? | 141 le01 wx with ODC.∋-p O X (nat→ω (ω→nat _ wx) ) |
142 ... | yes p = refl | |
143 ... | no ¬p = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where | |
144 le03 : x ≡ & (nat→ω (ω→nato wx)) | |
145 le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) ) | |
146 | |
147 ¬i0≡i1 : ¬ ( i0 ≡ i1 ) | |
148 ¬i0≡i1 () | |
149 | |
150 ¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 | |
151 ¬i0→i1 {i0} ne = ⊥-elim ( ne refl ) | |
152 ¬i0→i1 {i1} ne = refl | |
153 | |
154 ¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 | |
155 ¬i1→i0 {i0} ne = refl | |
156 ¬i1→i0 {i1} ne = ⊥-elim ( ne refl ) | |
142 | 157 |
143 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f | 158 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f |
144 fω→2-iso f = f-extensionality le01 where | 159 fω→2-iso f = f-extensionality (λ x → le01 x ) where |
145 le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x | 160 le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x |
146 le01 Zero = ? | 161 le01 x with ODC.∋-p O (fω→2 f) (nat→ω x) |
147 le01 (Suc x) = ? | 162 le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where |
163 le02 : infinite-d (& (* (& (nat→ω x)))) | |
164 le02 = proj1 (proj2 p ) | |
165 le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where | |
166 le04 : ¬ f x ≡ i1 | |
167 le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → infinite-d k) (sym &iso) (ω∋nat→ω {x}) , le05 ⟫ ⟫ where | |
168 le05 : (lt : infinite-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1 | |
169 le05 lt = trans (cong f (ω→nat-iso0 x lt (trans *iso *iso))) fx=1 | |
148 | 170 |
149 | |
150 |