Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/src/bijection.agda Mon Jun 26 15:52:14 2023 +0900 +++ b/src/bijection.agda Tue Jun 27 08:48:41 2023 +0900 @@ -57,6 +57,13 @@ -- famous diagnostic function -- +-- 1 1 0 1 0 ... +-- 0 1 0 1 0 ... +-- 1 0 0 1 0 ... +-- 1 1 1 1 0 ... + +-- 0 0 1 0 1 ... diag + diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool diag b n = not (fun← b n n) @@ -82,7 +89,7 @@ b-iso b = fiso← b _ -- --- ℕ <=> ℕ + 1 +-- ℕ <=> ℕ + 1 (infinite hotel) -- to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) to1 {n} {R} b = record {