Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/PFOD.agda @ 1174:375615f9d60f
Func and Funcs
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 18 Feb 2023 11:51:22 +0900 |
parents | d122d0c1b094 |
children | 362e43a1477c |
comparison
equal
deleted
inserted
replaced
1173:4b2f49a5a1d5 | 1174:375615f9d60f |
---|---|
142 ... | yes p = refl | 142 ... | yes p = refl |
143 ... | no ¬p = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where | 143 ... | no ¬p = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where |
144 le03 : x ≡ & (nat→ω (ω→nato wx)) | 144 le03 : x ≡ & (nat→ω (ω→nato wx)) |
145 le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) ) | 145 le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) ) |
146 | 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 ) | |
157 | |
158 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f | 147 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f |
159 fω→2-iso f = f-extensionality (λ x → le01 x ) where | 148 fω→2-iso f = f-extensionality (λ x → le01 x ) where |
160 le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x | 149 le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x |
161 le01 x with ODC.∋-p O (fω→2 f) (nat→ω x) | 150 le01 x with ODC.∋-p O (fω→2 f) (nat→ω 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 | 151 le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where |