# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615703516 -32400
# Node ID 0e87089e5de464a8e8e4b9cef15949727c50a6a5
# Parent  6835096cfa3aa79a2f82738d70ae3d555d5cc427
..`

diff -r 6835096cfa3a -r 0e87089e5de4 agda/halt.agda
--- a/agda/halt.agda	Sun Mar 14 08:27:05 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 15:31:56 2021 +0900
@@ -42,12 +42,12 @@
 
 --  ¬ A = A → ⊥ 
 
-diag :  (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ → Bool
+diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
-diagonal : ¬ Bijection  ( ℕ → Bool ) ℕ
-diagonal b = diagn1 (fun→ b (diag b) ) refl where
-    diagn1 : (n : ℕ ) → ¬ (fun→ b (diag b) ≡ n ) 
+diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
+diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
+    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
@@ -172,8 +172,8 @@
      lbisor [] = refl
      lbisor (false ∷ []) = refl
      lbisor (true ∷ []) = refl
-     lbisor (false ∷ true ∷ t) = ?
-     lbisor (false ∷ false ∷ t) = ?
+     lbisor (false ∷ true ∷ t) = {!!}
+     lbisor (false ∷ false ∷ t) = {!!}
      lbisor (true ∷ x ∷ t) = {!!}
 
 
@@ -204,7 +204,7 @@
          tmb1 x with is-tm x | inspect is-tm x
          ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
-TNℕ : Bijection  TM ℕ
+TNℕ : Halt → Bijection (TM → Bool) TM
 TNℕ = {!!}
 
 --  Halt1 (Halt2 x) ≡ x