# HG changeset patch # User Shinji KONO # Date 1687676296 -32400 # Node ID 003424a36fed3129a479cc049e5587cb1fb66c73 # Parent 0afcd5b995482a9e88c69bfd98527528aab658a2 is this agda's bug? diff -r 0afcd5b99548 -r 003424a36fed README.md --- a/README.md Sat Jun 24 08:56:47 2023 +0900 +++ b/README.md Sun Jun 25 15:58:16 2023 +0900 @@ -39,6 +39,8 @@ [OPair](https://shinji-kono.github.io/zf-in-agda/html/OPair.html) Orderd Pair and Direct Product +[bijection](https://shinji-kono.github.io/zf-in-agda/html/bijection.html) Bijection without HOD + ``` diff -r 0afcd5b99548 -r 003424a36fed src/bijection.agda --- a/src/bijection.agda Sat Jun 24 08:56:47 2023 +0900 +++ b/src/bijection.agda Sun Jun 25 15:58:16 2023 +0900 @@ -970,3 +970,33 @@ lem01 with cong proj2 eq ... | refl = refl +-- +-- ( Bool ∷ Bool ∷ [] ) ( Bool ∷ Bool ∷ [] ) ( Bool ∷ [] ) +-- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ [] + +-- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where + +LBBℕ : Bijection (List (List Bool)) ℕ +LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) + ? ? ? ? where + + atob : List (List Bool) → List Bool ∧ List Bool + atob [] = ⟪ [] , [] ⟫ + atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ + atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ + + btoa : List Bool ∧ List Bool → List (List Bool) + btoa ⟪ [] , _ ⟫ = [] + btoa ⟪ _ ∷ _ , [] ⟫ = [] + btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ + btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ + ... | [] = ( h ∷ [] ) ∷ [] + ... | x ∷ y = (h ∷ x ) ∷ y + +Lℕ=ℕ : Bijection (List ℕ) ℕ +Lℕ=ℕ = record { + fun→ = λ x → ? + ; fun← = λ n → ? + ; fiso→ = ? + ; fiso← = ? + } diff -r 0afcd5b99548 -r 003424a36fed src/cardinal.agda --- a/src/cardinal.agda Sat Jun 24 08:56:47 2023 +0900 +++ b/src/cardinal.agda Sun Jun 25 15:58:16 2023 +0900 @@ -1,6 +1,6 @@ {-# OPTIONS --allow-unsolved-metas #-} -open import Level +open import Level hiding (suc ; zero ) open import Ordinals module cardinal {n : Level } (O : Ordinals {n}) where @@ -9,7 +9,7 @@ import OD hiding ( _⊆_ ) import ODC -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat open import Relation.Binary.PropositionalEquality open import Data.Nat.Properties open import Data.Empty @@ -66,14 +66,18 @@ record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where field - ax : odef (* a) x - bx : odef (* b) (i→ iab _ ax) + y : Ordinal + ay : odef (* a) y + x=fy : x ≡ i→ iab _ ay Image : { a b : Ordinal } → Injection a b → HOD -Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = a ;