--- a/halt.agda	Wed Dec 02 23:03:39 2020 +0900
+++ b/halt.agda	Thu Dec 03 06:44:49 2020 +0900
@@ -13,16 +13,16 @@
 
 open import logic
 
-record Bijectionℕ {n : Level} (R : Set n)  : Set (Suc n) where
+record Bijection ℕ {n m : Level} (R : Set n) (S : Set m) : Set (Suc n) where
    field
-       fun←  :  ℕ → R
-       fun→  :  R → ℕ
+       fun←  :  S → R
+       fun→  :  R → S
        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
-       fiso→ : (x : ℕ ) → fun→ ( fun← x )  ≡ x 
+       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
 
-open Bijectionℕ
+open Bijection ℕ
 
-diagonal : ¬ Bijectionℕ ( ℕ → Bool )
+diagonal : ¬ Bijection ℕ ( ℕ → Bool )
 diagonal b = diagn1 (fun→ b diag) refl where
     diag :  ℕ → Bool
     diag n = not (fun← b n n)
@@ -39,20 +39,20 @@
            diag n 
         ∎ ) where open ≡-Reasoning
 
-to1 : {n : Level} {R : Set n} → Bijectionℕ R → Bijectionℕ (⊤ ∨ R )
+to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
 to1 = {!!}
 
-ton : {n : Level} {R : Set n} → Bijectionℕ R → Bijectionℕ (ℕ ∨ R )
+ton : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (ℕ ∨ R )
 ton = {!!}
 
-to∨ : {n : Level} {R S : Set n} → Bijectionℕ R → Bijectionℕ S → Bijectionℕ (S ∨ R )
+to∨ : {n : Level} {R S : Set n} → Bijection ℕ R → Bijection ℕ S → Bijection ℕ (S ∨ R )
 to∨ = {!!}
 
-to⊤ : Bijectionℕ ( List ⊤ )
+to⊤ : Bijection ℕ ( List ⊤ )
 to⊤ = {!!}
 
 {-# TERMINATING #-}
-to2 : Bijectionℕ ( List Bool )
+to2 : Bijection ℕ ( List Bool )
 to2 = record {
        fun← = λ n → l→ (n← n)
      ; fun→  = λ x → b→ (b← x)
@@ -82,7 +82,35 @@
            x
         ∎  where open ≡-Reasoning
 
+TM   : Set
+TM   = List Bool → Bool
+
+postulate
+   utm         : List Bool → TM
+   tm-encode   : TM → List Bool 
+   utm-correct : (x : List Bool) → (t : TM) → t x <=> utm (tm-encode t) x
+
+tmb : Bijection ℕ TM
+tmb = record {
+       fun← = λ n → utm (fun← to2)
+     ; fun→  = λ x → fun→ to2 (tm-encode x)
+     ; fiso← = {!!} 
+     ; fiso→ = {!!} 
+  }
+
+nonexistence-of-halt : (halt : TM → List Bool → Bool) → Bijection ℕ (ℕ → Bool)
+nonexistence-of-halt = ? where
+   not-halt : TM 
+   not-halt x = not (halt (utm x))
+
+nonexistence-of-halt : ¬ (TM → List Bool → Bool) 
+nonexistence-of-halt halt = ? where
+   not-halt : TM 
+   not-halt x = not (halt (utm x))
 
 
 
 
+
+
+