--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/halt.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -0,0 +1,102 @@
+module halt where
+
+open import Level renaming ( zero to Zero ; suc to Suc )
+open import Data.Nat
+open import Data.List hiding ([_])
+open import Data.Nat.Properties
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Unit
+open import  Relation.Binary.Core
+open import  Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+
+open import logic
+
+record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+   field
+       fun←  :  S → R
+       fun→  :  R → S
+       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
+       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
+
+open Bijection 
+
+diagonal : ¬ Bijection  ( ℕ → Bool ) ℕ
+diagonal b = diagn1 (fun→ b diag) refl where
+    diag :  ℕ → Bool
+    diag n = not (fun← b n n)
+    diagn1 : (n : ℕ ) → ¬ (fun→ b diag ≡ n ) 
+    diagn1 n dn = ¬t=f (diag n ) ( begin
+           not diag n 
+        ≡⟨⟩
+           not (not fun← b n n)
+        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
+           not (fun← b (fun→ b diag)  n)
+        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
+           not (fun← b n n)
+        ≡⟨⟩
+           diag n 
+        ∎ ) where open ≡-Reasoning
+
+to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
+to1 {n} {R} b = record {
+       fun←  = to11
+     ; fun→  = to12
+     ; fiso← = to13
+     ; fiso→ = to14
+   } where
+       to11 : ⊤ ∨ R → ℕ
+       to11 (case1 tt) = 0
+       to11 (case2 x) = suc ( fun← b x )
+       to12 : ℕ → ⊤ ∨ R
+       to12 zero = case1 tt
+       to12 (suc n) = case2 ( fun→ b n)
+       to13 : (x : ℕ) → to11 (to12 x) ≡ x
+       to13 zero = refl
+       to13 (suc x) = cong suc (fiso← b x)
+       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
+       to14 (case1 x) = refl
+       to14 (case2 x) = cong case2 (fiso→ b x)
+
+open _∧_
+
+--   []     case1
+--   0    → case2 10   
+--   0111 → case2 10111
+--
+LBℕ : Bijection  ( List Bool ) ℕ
+LBℕ = {!!}
+
+postulate
+   utm         : List Bool → List Bool → Bool
+
+open import Axiom.Extensionality.Propositional
+postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 
+
+record TM : Set where
+   field
+      tm : List Bool → Bool
+      encode : List Bool
+      is-tm : utm encode ≡ tm
+
+open TM
+
+tm-cong : {x y : TM} → tm x ≡ tm y → encode x ≡ encode y → is-tm x ≅ is-tm y → x ≡ y
+tm-cong refl refl refl  = refl
+
+tm-bij :  Bijection TM (List Bool)
+tm-bij = record {
+       fun←  = λ x → record { tm = utm x ; encode = x ; is-tm = refl }
+     ; fun→  = λ tm → encode tm
+     ; fiso← = tmb1
+     ; fiso→ = λ x → refl
+    }  where
+         tmb1 : (x : TM ) →  record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x
+         tmb1 x with is-tm x | inspect is-tm x
+         ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
+
+halting : (halt : TM → List Bool  → Bool ) → (z : TM) →  ¬ ((x : TM) → tm z ≡ (λ y → halt x y ) )
+halting halt z halting = {!!}
+