対角線論法とHalting Problem

対角線論法は割と簡単に(やっと)書けたのだが、Halting 問題の方は良くわからない。

　　 Bijection TM (List Bool)

自体が矛盾するので、 TM = List Bool → Bool にしないで、そのうちの encode を持つものみたいに限定するのだろうな。
で、halt が encode を持つとすると矛盾くらいか。いや、そう書こうとしているんですが...

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
　　¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
　　¬t=f true ()
　　¬t=f false ()
　　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