--- a/src/cardinal.agda	Wed Jul 05 12:09:48 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 12:32:31 2023 +0900
@@ -348,29 +348,20 @@
      b : HODBijection (Power S) S 
      b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)
 
-     record inS : Set n where
-        field
-           x : Ordinal
-           sx : odef S x
+     data inS : Set n  where
+         ins : (x : Ordinal) (sx : odef S x) → inS
 
-     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
+     xinS : inS → Ordinal
+     xinS (ins x sx) = x
 
-     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
+     inS-eq : {x y : inS} → xinS x ≡ xinS y → x ≡ y
+     inS-eq {ins x sx} {ins .(xinS (ins x sx)) sy} refl = cong (λ k → ins x k ) ( HE.≅-to-≡ ( ∋-irr {S} sx sy ))  
 
-           -- 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
+     data inSC (ib : inS → Bool) (x : Ordinal) : Set n where
+         insc : (sx  : odef S x) (tsx : ib (ins x sx) ≡ true) → inSC ib x 
 
-     record inSC (ib : inS → Bool) (x : Ordinal) : Set n where
-        field
-           sx  : odef S x
-           tsx : ib record { x = x ; sx = sx } ≡ true
+     import Axiom.Extensionality.Propositional
+     postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
      BS : Bijection (inS → Bool ) inS
      BS = record {
@@ -380,19 +371,21 @@
        ; 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 ) )
+           ca00 (ins x sx) (ins y sy) with ODC.p∨¬p O ( odef (* ( fun← b x sx)) y )
            ... | case1 y = true
            ... | case2 n  = false
            ca01 : (inS → Bool) → inS
-           ca01 ib = record { x = fun→ b (& ca03) ca02 ; sx = funB b (& ca03) ca02 } where
+           ca01 ib = ins (fun→ b (& ca03) ca02) (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)
+               ca02 z xz = ? -- inSC.sx (subst (λ k → odef k z) *iso xz)
+           ca06 : (ib : inS → Bool) → (z : inS) →  ca00 (ca01 ib) z ≡ ib z 
+           ca06 = ?
            ca04 : (ib : inS → Bool) → ca00 (ca01 ib) ≡ ib
-           ca04 ib = ?
+           ca04 ib = f-extensionality (λ z → ca06 ib z )
            ca05 : (x : inS) → ca01 (ca00 x) ≡ x
-           ca05 x = ?
+           ca05 (ins x sx) = inS-eq ?
 
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )