Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/bijection.agda @ 1393:c67ecdf89e77
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 27 Jun 2023 08:48:41 +0900 |
| parents | 003424a36fed |
| children | 5d69ed581269 |
comparison
equal
deleted
inserted
replaced
| 1392:8645a167d76b | 1393:c67ecdf89e77 |
|---|---|
| 54 | 54 |
| 55 -- ¬ A = A → ⊥ | 55 -- ¬ A = A → ⊥ |
| 56 -- | 56 -- |
| 57 -- famous diagnostic function | 57 -- famous diagnostic function |
| 58 -- | 58 -- |
| 59 | |
| 60 -- 1 1 0 1 0 ... | |
| 61 -- 0 1 0 1 0 ... | |
| 62 -- 1 0 0 1 0 ... | |
| 63 -- 1 1 1 1 0 ... | |
| 64 | |
| 65 -- 0 0 1 0 1 ... diag | |
| 59 | 66 |
| 60 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool | 67 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool |
| 61 diag b n = not (fun← b n n) | 68 diag b n = not (fun← b n n) |
| 62 | 69 |
| 63 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S | 70 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S |
| 80 | 87 |
| 81 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) | 88 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) |
| 82 b-iso b = fiso← b _ | 89 b-iso b = fiso← b _ |
| 83 | 90 |
| 84 -- | 91 -- |
| 85 -- ℕ <=> ℕ + 1 | 92 -- ℕ <=> ℕ + 1 (infinite hotel) |
| 86 -- | 93 -- |
| 87 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) | 94 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) |
| 88 to1 {n} {R} b = record { | 95 to1 {n} {R} b = record { |
| 89 fun← = to11 | 96 fun← = to11 |
| 90 ; fun→ = to12 | 97 ; fun→ = to12 |