# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685944202 -32400
# Node ID c97660e1953562ad7d47610b4a794919688839ba
# Parent  9e26c9abfafb83754a1d2219fb3d179f0ac16cb5
...

diff -r 9e26c9abfafb -r c97660e19535 src/bijection.agda
--- a/src/bijection.agda	Mon Jun 05 11:33:27 2023 +0900
+++ b/src/bijection.agda	Mon Jun 05 14:50:02 2023 +0900
@@ -1,5 +1,8 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
 module bijection where
 
+
 open import Level renaming ( zero to Zero ; suc to Suc )
 open import Data.Nat
 open import Data.Maybe
@@ -471,3 +474,58 @@
 
         lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
         lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) 
+
+Bernstein : (A B C D : Set) → Bijection A D → Bijection C D → (f : A → B ) → (g : B → C )  → Bijection B D
+Bernstein A B C D ad cd f g = ?
+
+bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
+bi-∧ {A} {B} {C} {D} ab cd = record {
+       fun←  = λ x → ⟪ fun←  ab (proj1 x) , fun←  cd (proj2 x) ⟫
+     ; fun→  = λ n → ⟪ fun→  ab (proj1 n) , fun→  cd (proj2 n) ⟫
+     ; fiso← = lem0
+     ; fiso→ = lem1
+  } where 
+      open Bijection 
+      lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x
+      lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y)   
+      lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x
+      lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y)   
+
+
+LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ
+LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ)  ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn)
+
+LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ
+LMℕ A Ln = Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) ℕ Ln (LM1 A Ln)  f g where
+   f : List A → List (Maybe A)
+   f [] = []
+   f (x ∷ t) = just x ∷ f t
+   g : List (Maybe A) → List A ∧ List Bool
+   g [] = ⟪ [] , [] ⟫
+   g (just h ∷ t)  = ⟪ h ∷ proj1 (g t) , true  ∷ proj2 (g t) ⟫
+   g (nothing ∷ t) = ⟪     proj1 (g t) , false ∷ proj2 (g t) ⟫
+
+-- open import Data.Fin
+--
+--- record LF (n m : ℕ) (lton : List (Fin n) → ℕ ) : Set where
+---   field
+---      nlist : List Bool
+---      isBin : lton nlist ≡ m
+---      isUnique :  (x : List Bool) → lton x ≡ m → nlist  ≡ x 
+--- 
+--- lb+1 : {n : ℕ) → List Bool → List Bool
+--- lb+1 [] =  false ∷ [] 
+--- lb+1 (false ∷ t) = true ∷ t 
+--- lb+1 (true ∷ t) =  false ∷ lb+1 t
+--- 
+--- lb-1 : {n : ℕ) → List Bool → List Bool
+--- lb-1 [] =  []
+--- lb-1 (true ∷ t) = false ∷ t 
+--- lb-1 (false ∷ t) with lb-1 t
+--- ... | [] = true ∷ []
+--- ... | x ∷ t1 = true ∷ x ∷ t1
+
+--- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n)) 
+--- LBFin = ?
+
+--