Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/bijection.agda @ 1387:003424a36fed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is this agda's bug?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 25 Jun 2023 15:58:16 +0900
parents 0afcd5b99548
children c67ecdf89e77
comparison
equal deleted inserted replaced
1386:0afcd5b99548 1387:003424a36fed
968 lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where 968 lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where
969 lem01 : proj2 (g a) ≡ bt 969 lem01 : proj2 (g a) ≡ bt
970 lem01 with cong proj2 eq 970 lem01 with cong proj2 eq
971 ... | refl = refl 971 ... | refl = refl
972 972
973 --
974 -- ( Bool ∷ Bool ∷ [] ) ( Bool ∷ Bool ∷ [] ) ( Bool ∷ [] )
975 -- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ []
976
977 -- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where
978
979 LBBℕ : Bijection (List (List Bool)) ℕ
980 LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ))
981 ? ? ? ? where
982
983 atob : List (List Bool) → List Bool ∧ List Bool
984 atob [] = ⟪ [] , [] ⟫
985 atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫
986 atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫
987
988 btoa : List Bool ∧ List Bool → List (List Bool)
989 btoa ⟪ [] , _ ⟫ = []
990 btoa ⟪ _ ∷ _ , [] ⟫ = []
991 btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫
992 btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫
993 ... | [] = ( h ∷ [] ) ∷ []
994 ... | x ∷ y = (h ∷ x ) ∷ y
995
996 Lℕ=ℕ : Bijection (List ℕ) ℕ
997 Lℕ=ℕ = record {
998 fun→ = λ x → ?
999 ; fun← = λ n → ?
1000 ; fiso→ = ?
1001 ; fiso← = ?
1002 }