# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688526588 -32400
# Node ID 3e50aa63f550feebce356f262d333425746c7fab
# Parent  a295c52af3b725d29fdbd2fd3e226cf23a0bca76
...

diff -r a295c52af3b7 -r 3e50aa63f550 src/cardinal.agda
--- a/src/cardinal.agda	Wed Jul 05 10:57:43 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 12:09:48 2023 +0900
@@ -335,7 +335,7 @@
 --    t   true  false   ...  false
 ---
 Cantor1 : { S : HOD } → S c< Power S
-Cantor1 {S}  f = diag4 where 
+Cantor1 {S}  f = ? where 
      f1 : Injection (& S) (& (Power S))
      f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = ? }where
          c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
@@ -348,42 +348,52 @@
      b : HODBijection (Power S) S 
      b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)
 
-     diag2 : {x : Ordinal } → (sx : odef S x) → (z : Ordinal) → odef (* (fun← b x sx)) z → odef S z
-     diag2 {x} sx z xz = funA b x sx z xz 
-    
-     diag3 : {x : Ordinal } → (sx : odef S x) → odef (Power S) (fun← b x sx)
-     diag3 sx = diag2 sx
+     record inS : Set n where
+        field
+           x : Ordinal
+           sx : odef S x
+
+     ins-refl : (x : inS) → record { x = inS.x x ; sx = inS.sx x } ≡ x
+     ins-refl x with HE.≅-to-≡ ( ∋-irr {S} (inS.sx x) (inS.sx x) )
+     ... | refl = refl
 
-     diag : {x : Ordinal } → (sx : odef S x) → (z : Ordinal) → Set n
-     diag {x} sx z with trio< x z | ODC.p∨¬p O ( odef (* (fun← b x sx)) x)
-     ... | tri< a ¬b ¬c | n = odef  (* (fun← b x sx)) z 
-     ... | tri> ¬a ¬b c | n = odef  (* (fun← b x sx)) z 
-     ... | tri≈ ¬a b₁ ¬c | case1 y = ¬ odef S z
-     ... | tri≈ ¬a b₁ ¬c | case2 n = odef S z
+     inS-eq : {x y : inS } → inS.x x ≡ inS.x y  → x ≡ y  
+     inS-eq {x} {y} eq = ? where -- HE.≅-to-≡ (ca11 (inS.sx x) (inS.sx y) eq ?) where
+         ca11 : {x y : Ordinal} →  (sx1 : odef S x) (sy1 : odef S y)  → x ≡ y → sx1 ≅ sy1 
+             →  record { x = x ; sx = sx1 }  ≅ record { x = y ; sx = sy1 } 
+         ca11 _ _ refl HE.refl = HE.refl
 
-     DIAG : {x : Ordinal } → (sx : odef S x) → HOD
-     DIAG {x} sx = record { od = record { def = λ z → diag sx z  } ; odmax = ? ; <odmax = ? } 
+           -- cong₂ (λ j k → record { x = j ; sx = k }) eq ( HE.≅-to-≡ ( ∋-irr {S} (inS.sx x) (inS.sx y) ))  
+           -- ca11 : inS.x x ≡ inS.x y → inS.sx x ≅ inS.sx y → x ≡ y
+           -- ca11 refl refl = refl
 
-     Pdiag : {x : Ordinal} → (sx : odef S x) → odef (Power S) (& (DIAG sx))
-     Pdiag {x} sx z xz with trio< x z | ODC.p∨¬p O ( odef (* (fun← b x sx)) x) | subst (λ k → odef k z) *iso xz
-     ... | tri< a ¬b ¬c | n | u = funA b x sx z u
-     ... | tri> ¬a ¬b c | n | u = funA b x sx z u
-     ... | tri≈ ¬a refl ¬c | case1 x₁ | u = ⊥-elim ( u sx )
-     ... | tri≈ ¬a refl ¬c | case2 x₁ | u = u
-
-     p0 : odef (Power S) o∅
-     p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
+     record inSC (ib : inS → Bool) (x : Ordinal) : Set n where
+        field
+           sx  : odef S x
+           tsx : ib record { x = x ; sx = sx } ≡ true
 
-     s : Ordinal 
-     s = fun→ b o∅ p0
+     BS : Bijection (inS → Bool ) inS
+     BS = record {
+         fun←  = ca00
+       ; fun→  = ca01
+       ; fiso← = ca04
+       ; fiso→ = ca05 
+       } where
+           ca00 : inS → inS → Bool
+           ca00 ix iy with ODC.p∨¬p O ( odef (* ( fun← b (inS.x ix ) (inS.sx ix))) (inS.x iy ) )
+           ... | case1 y = true
+           ... | case2 n  = false
+           ca01 : (inS → Bool) → inS
+           ca01 ib = record { x = fun→ b (& ca03) ca02 ; sx = funB b (& ca03) ca02 } where
+               ca03 : HOD
+               ca03 = record { od = record { def = λ x → inSC ib x } ; odmax =　? ; <odmax = ? }
+               ca02 : odef (Power S) (& ca03)
+               ca02 z xz = inSC.sx (subst (λ k → odef k z) *iso xz)
+           ca04 : (ib : inS → Bool) → ca00 (ca01 ib) ≡ ib
+           ca04 ib = ?
+           ca05 : (x : inS) → ca01 (ca00 x) ≡ x
+           ca05 x = ?
 
-     ss : odef S s
-     ss = funB b o∅ p0
-
-     diag4 : ⊥ 
-     diag4 with ODC.p∨¬p O ( odef (* (fun← b s ss)) s)
-     ... | case1 y  = ?
-     ... | case2 n  = ?
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}