# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719644258 -32400
# Node ID 88fdc41868f9d07995c5b6044f775014200ee621
# Parent  32001d93755b155b31437673f2bb09f1fe9caeff
...

diff -r 32001d93755b -r 88fdc41868f9 src/OD.agda
--- a/src/OD.agda	Fri Jun 28 20:55:38 2024 +0900
+++ b/src/OD.agda	Sat Jun 29 15:57:38 2024 +0900
@@ -336,7 +336,7 @@
 record RXCod (X COD : HOD) (ψ : (x : HOD) → X ∋ x → HOD)  : Set (suc n) where
  field
      ≤COD : ∀ {x : HOD } → (lt : X ∋ x) → ψ x lt ⊆ COD 
-     ψ-eq : ∀ {x : HOD } → (lt lt1 : X ∋ x) → ψ x lt ≡ ψ x lt1
+     ψ-eq : ∀ {x : HOD } → (lt lt1 : X ∋ x) → ψ x lt =h= ψ x lt1
 
 record Replaced1 (A : HOD) (ψ : (x : Ordinal ) → odef A x → Ordinal ) (x : Ordinal ) : Set n where
    field
@@ -380,12 +380,12 @@
             (λ z xz → & (ψ (* z) (eq→ *iso (subst (odef (* (& X))) (sym &iso) xz)))) x →
             Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x
       ri0 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = eq→  *iso az 
-          ; x=ψz = trans x=ψz (cong (&) (RXCod.ψ-eq rc _ _ ))  } 
+          ; x=ψz = trans x=ψz (==→o≡ (RXCod.ψ-eq rc _ _ )) } 
       ri1 : {x : Ordinal} → 
             Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x →
               Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (eq→ *iso (subst (odef (* (& X))) (sym &iso) xz)))) x 
       ri1 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = eq←  *iso az 
-          ; x=ψz = trans x=ψz (cong (&) (RXCod.ψ-eq rc _ _ ))  } 
+          ; x=ψz = trans x=ψz (==→o≡  (RXCod.ψ-eq rc _ _ ))  } 
 
 _∈_ : ( A B : HOD  ) → Set n
 A ∈ B = B ∋ A
diff -r 32001d93755b -r 88fdc41868f9 src/ZProduct.agda
--- a/src/ZProduct.agda	Fri Jun 28 20:55:38 2024 +0900
+++ b/src/ZProduct.agda	Sat Jun 29 15:57:38 2024 +0900
@@ -190,6 +190,10 @@
 proj1 (ZFP⊆ {A} {B} {a} a⊆A)  (ab-pair x x₁) = ab-pair (a⊆A x) x₁
 proj2 (ZFP⊆ {A} {B} {a} a⊆A)  (ab-pair x x₁) = ab-pair x (a⊆A x₁) 
 
+ZFP-cong : {A B C D  : HOD} → A =h= C → B =h= D → ZFP A B =h= ZFP C D
+eq→ (ZFP-cong {A} {B} {C} {D} a=c b-d ) {w} (ab-pair x y) = ab-pair (eq→ a=c x) (eq→ b-d y)
+eq← (ZFP-cong {A} {B} {C} {D} a=c b-d ) {w} (ab-pair x y) = ab-pair (eq← a=c x) (eq← b-d y)
+
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → odef (ZFP A B) k ) (==→o≡ (prod-cong-== *iso *iso ) ) (ab-pair aa bb) 
 
@@ -319,6 +323,10 @@
 ZP-proj1⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc
 ... | ab-pair {a} {b} aa bb = ab-pair record { b = _ ; aa = aa ; bb = bb ; c∋ab = cc }  bb
 
+ZP-proj1-cong : {A B C : HOD} → {cab1 cab2 : C ⊆ ZFP A B} → ZP-proj1 A B C cab1 =h= ZP-proj1 A B C cab2 
+eq→ (ZP-proj1-cong {A} {B} {C} {cab1} {cab2}) {w} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } 
+eq← (ZP-proj1-cong {A} {B} {C} {cab1} {cab2}) {w} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } 
+
 ZP-proj1=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef B b → a ⊆ A → m =h= ZFP a B → a =h= ZP-proj1 A B m cab 
 ZP-proj1=rev {A} {B} {a} {m} {b} {cab} bb a⊆A m=aB = record { eq→ = zp00 ; eq← = zp01 } where
      zp00 : {x : Ordinal} → odef a x → ZP1 A B m cab x
@@ -329,12 +337,12 @@
         zp02 {z} eq mab with eq→  m=aB mab 
         ... | ab-pair {w1} {w2} aw1 bw2 = subst (λ k → odef a k ) (proj1 (prod-≡ eq )) aw1
 
-ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab ≡ od∅ → z ≡ & od∅
+ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab =h= od∅ → z ≡ & od∅
 ZP-proj1-0 {A} {B} {z} {zab} eq = uf10 where
          uf10 : z ≡ & od∅
          uf10 = trans (sym &iso) ( ¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) ) where
              uf11 : {y : Ordinal } → odef (* z) y → ⊥ 
-             uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ1 pqy)) eq uf12  ) ) where
+             uf11 {y} zy = ⊥-elim ( ¬x<0 (eq→ eq uf12  ) ) where
                 pqy : odef (ZFP A B) y
                 pqy = zab zy
                 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >)
@@ -352,6 +360,10 @@
 ZP-proj2 : (A B C : HOD) → C  ⊆ ZFP A B → HOD
 ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) } 
 
+ZP-proj2-cong : {A B C : HOD} → {cab1 cab2 : C ⊆ ZFP A B} → ZP-proj2 A B C cab1 =h= ZP-proj2 A B C cab2 
+eq→ (ZP-proj2-cong {A} {B} {C} {cab1} {cab2}) {w} record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } 
+eq← (ZP-proj2-cong {A} {B} {C} {cab1} {cab2}) {w} record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } 
+
 ZP-proj2⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP A (ZP-proj2 A B C cab) 
 ZP-proj2⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc
 ... | ab-pair {a} {b} aa bb = ab-pair aa record { a = _ ; aa = aa ; bb = bb ; c∋ab = cc }  
@@ -388,8 +400,8 @@
     fodmax = record { ≤COD = λ {x} ax →  lemma1 ax ; ψ-eq = lemma2 } where
         lemma1 : {x : HOD} → (ax : odef A (& x)) → < x , * (func ax) > ⊆ Power (Union (A , B)) 
         lemma1 {x} ax = ZFP<AB ax (subst (λ k → odef B k) (sym &iso) ( is-func ax ) )
-        lemma2 : {x : HOD} (lt lt1 : A ∋ x) → < x , * (func lt) > ≡ < x , * (func lt1) >
-        lemma2 {x} lt1 lt2 = cong ( λ k → < x , * k > ) (func-wld lt1 lt2 refl )
+        lemma2 : {x : HOD} (lt lt1 : A ∋ x) → < x , * (func lt) > =h= < x , * (func lt1) >
+        lemma2 {x} lt1 lt2 = prod-cong-== ==-refl (o≡→== (func-wld lt1 lt2 refl ))
 
 
 data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
diff -r 32001d93755b -r 88fdc41868f9 src/filter-util.agda
--- a/src/filter-util.agda	Fri Jun 28 20:55:38 2024 +0900
+++ b/src/filter-util.agda	Sat Jun 29 15:57:38 2024 +0900
@@ -49,10 +49,10 @@
 
 filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
     → odef x z → odef (ZFP P Q) z
-filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) ? xz )
+filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (eq← *iso xz)
 
 rcp :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx))
-rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly }
+rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly ; ψ-eq = λ {x} fx1 fx2  → ZP-proj1-cong }
 
 Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
@@ -65,62 +65,58 @@
     isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q
     isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) 
     fp00 : FP ⊆ Power P 
-    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw
-    ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with eq→ *iso ( subst (λ k → odef (* k) w) x=ψz xw )
+    ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
     f0 :  {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
     f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q 
     f1 :  {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q
     f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where
        PQq : Power (ZFP P Q) ∋ ZFP q Q
-       PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans ? (cong (λ k → ZFP k Q) ?)) zpq )
+       PQq z zpq = isP→PxQ {* (& q)} (Pq _) (eq→ (ZFP-cong (==-sym *iso) ==-refl) ( eq→ *iso zpq ))
        q⊆P : q ⊆ P
-       q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym ?) qw )
+       q⊆P {w} qw = Pq _ (eq← *iso qw ) 
        p⊆P : p ⊆ P
        p⊆P {w} pw = q⊆P (p⊆q pw)
        p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)))
        p=proj1 = x=ψz
        p⊆ZP : (* z) ⊆ ZFP p Q
-       p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP 
+       p⊆ZP lt = eq→ (ZFP-cong (==-sym ( ord→== p=proj1  )) ==-refl ) (ZP-proj1⊆ZFP lt)
        ty05 : filter F ∋  ZFP p Q
-       ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) ? wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
+       ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
        ty06 : ZFP p Q ⊆ ZFP q Q
        ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
        fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q
        fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq
        q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06))))
-       q=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso )
+       q=proj1 = ==→o≡ (ZP-proj1=rev (zp2 pqa) q⊆P *iso )
     f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q)
     f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq 
          = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where
        p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P
-       p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) ? px
-       ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+       p⊆P {zp} {p} fzp p=proj1 {x} px with eq→ (ord→== p=proj1) px
+       ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
        x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q
-       x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP
+       x⊆pxq {zp} {p} fzp p=proj1 lt = eq→ (ZFP-cong (==-sym ( ord→== p=proj1  )) ==-refl ) (ZP-proj1⊆ZFP lt)
        ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
        ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
          pqz :  odef (ZFP (p ∩ q) Q)  z
-         pqz = ? -- subst (λ k → odef k z ) (trans ? (sym (proj1 ZFP∩) ))  xz
+         pqz = eq← (proj1 ZFP∩) (eq→ *iso xz) 
          pqz1 : odef P (zπ1 pqz)
          pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz))
          pqz2 : odef Q (zπ2 pqz)
          pqz2 = zp2 pqz
        ty53 : filter F ∋ ZFP p Q
-       ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp)
-         ?)
-         ? ? -- (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
+       ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) (eq→ *iso wz )) (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
        ty52 : filter F ∋ ZFP q Q
-       ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq)
-         ?)
-         ? (x⊆pxq fzq x=ψzq)
+       ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
        ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
        ty51 = filter2 F ty53 ty52 ty54
        ty50 : filter F ∋ ZFP (p ∩ q) Q
-       ty50 = subst (λ k → filter F ∋ k ) ? ty51
+       ty50 = subst (λ k → odef (filter F)  k ) (sym (==→o≡ (proj1 ZFP∩))) ty51
        pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50)))
-       pq=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) ? pqx)) *iso )
+       pq=proj1  = ==→o≡ (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (eq← *iso pqx)) *iso )
 
 Filter-Proj1-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a )
       → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
@@ -129,29 +125,31 @@
        FP = Filter-Proj1 pqa F
        ty60 : ¬ (filter FP ∋ od∅)
        ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF 
-          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) ? x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
+          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (eq→ *iso x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
            ty61 : * z ⊆  od∅
-           ty61 {x} lt = ? -- ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj1-0 (sym ?))) *iso)  lt ))
+           ty61 {x} lt = ⊥-elim (¬x<0 ty62 ) where
+               ty62 : odef od∅ x
+               ty62 = eq→ *iso (subst (λ k → odef (* k) x) (ZP-proj1-0 (ord→== (sym x=ψz))  ) lt )
        ty62 :  {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (filter (Filter-Proj1 pqa F) ∋ p) ∨ (filter (Filter-Proj1 pqa F) ∋ (P ＼ p))
        ty62 {p} Pp NEGP = uf05  where
              p⊆P : p ⊆ P
-             p⊆P {z} px = Pp _ (subst (λ k → odef k z) ? px)
+             p⊆P {z} px = Pp _ (eq← *iso px)
              mp : HOD
              mp = ZFP p Q 
              uf03 : Power (ZFP P Q) ∋  mp
-             uf03 x xz with subst (λ k → odef k x ) ? xz
-             ... | t = ? -- ab-pair ax by = ab-pair (p⊆P ax) by
+             uf03 x xz with eq→ *iso xz
+             ... | ab-pair ax by = ab-pair (p⊆P ax) by
              uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp)
-             uf04 x xz = ? -- proj1 (subst (λ k → odef k x) *iso xz)
+             uf04 x xz = proj1 (eq→ *iso xz) 
              uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp))
              uf02 = ultra-filter.ultra UF uf03 uf04
              uf05 : (filter FP ∋ p) ∨ (filter FP ∋ (P ＼ p))
              uf05 with uf02
-             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = ?  }
-             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ? }
+             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = ==→o≡ (ZP-proj1=rev (zp2 pqa) p⊆P *iso ) }
+             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ==→o≡ (ZP-proj1=rev (zp2 pqa) proj1 (==-trans *iso (proj1 ZFP\Q))) } 
 
 rcq :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) Q (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx))
-rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly }
+rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly ; ψ-eq = λ {x} fx1 fx2  → ZP-proj2-cong }
 
 --
 -- Proj2 can be dervie from symmetry of ZFP (Product)
diff -r 32001d93755b -r 88fdc41868f9 src/maximum-filter.agda
--- a/src/maximum-filter.agda	Fri Jun 28 20:55:38 2024 +0900
+++ b/src/maximum-filter.agda	Sat Jun 29 15:57:38 2024 +0900
@@ -1,47 +1,52 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
 
 open import Level
 open import Ordinals
-module maximum-filter {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+open import Relation.Nullary
+module maximum-filter {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom )
+       (AC : OD.AxiomOfChoice O HODAxiom ) where
+
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 open import logic
-import OD 
-
-open import Relation.Nullary 
-open import Data.Empty 
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-import BAlgebra 
-
-open BAlgebra O
+open import nat
 
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
--- open Ordinals.IsNext isNext
 open OrdUtil O
-open ODUtil O
-
-
-import ODC
-open ODC O
+open ODUtil O HODAxiom  ho<
 
 open _∧_
 open _∨_
 open Bool
 
-open import filter O
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+open import filter O HODAxiom ho< AC
+open import ZProduct O HODAxiom ho<
 
 open Filter
 
-
-open import  Relation.Binary
 open import  Relation.Binary.Structures
 
 PO : IsStrictPartialOrder _≡_ _⊂_ 
diff -r 32001d93755b -r 88fdc41868f9 src/zorn.agda
--- a/src/zorn.agda	Fri Jun 28 20:55:38 2024 +0900
+++ b/src/zorn.agda	Sat Jun 29 15:57:38 2024 +0900
@@ -1,11 +1,56 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-open import Level hiding ( suc ; zero )
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level renaming (zero to Zero ; suc to Suc)
 open import Ordinals
+open import logic
+open import Relation.Nullary
+
+open import Ordinals
+import HODBase
+import OD
+open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-import OD 
-module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+module zorn {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom )
+       (AC : OD.AxiomOfChoice O HODAxiom ) 
+        (_<_ : (x y : OD.HOD O HODAxiom) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
+
+
+-- open import  Relation.Binary.Structures
+open import Data.Empty
+open import Data.Nat hiding ( _≤_  ; _<_ )
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
+
+open import logic
+open import nat
+
+open OrdUtil O
+open ODUtil O HODAxiom  ho<
+
+open _∧_
+open _∨_
+open Bool
+
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+open import filter O HODAxiom ho< AC
+open import ZProduct O HODAxiom ho<
+
+open Filter
+
 
 --
 -- Zorn-lemma : { A : HOD }
@@ -14,35 +59,6 @@
 --     → Maximal A
 --
 
-open import logic
-
-open import Relation.Nullary
-open import Data.Empty
-import BAlgebra
-
-open import Data.Nat hiding ( _<_ ; _≤_ )
-open import Data.Nat.Properties
-open import nat
-
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
--- open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
-
-import ODC
-
-open _∧_
-open _∨_
-open Bool
-
-open HOD
 
 --
 -- Partial Order on HOD ( possibly limited in A )
@@ -85,7 +101,7 @@
 
 ptrans =  IsStrictPartialOrder.trans PO
 
-open _==_
+-- open _==_
 -- open _⊆_ -- we use different definition
 
 -- We cannot prove this without Well foundedness of A
@@ -402,8 +418,8 @@
    --
    -- supf a over b and supf a is not included in UnionCF a nor UnionCF b, so UnionCF b is equal to the UnionCF a
    --
-   union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
-   union-max {a} {b} b≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+   union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a =h= UnionCF A f ay supf b
+   union-max {a} {b} b≤sa b≤z sa<sb = record { eq→ = z47 ; eq← = z48 } where
           z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
           z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
           z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
@@ -422,7 +438,7 @@
    x≤supfx→¬sa<sa : {a b : Ordinal } → b o≤ z → b o≤ supf a → ¬ (supf a o< supf b )
    x≤supfx→¬sa<sa {a} {b} b≤z b≤sa sa<sb = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x o≤ supf a ∧ supf a o< supf b → ⊥, because it defines the same UnionCF
          z27 : supf a ≡ supf b
-         z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ( union-max  b≤sa b≤z sa<sb)
+         z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ? -- ( union-max  b≤sa b≤z sa<sb)
 
    order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
    order {a} {b} {w} b≤z sa<sb fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
@@ -448,7 +464,7 @@
 
    f-total : IsTotalOrderSet chain
    f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
-     subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
+     subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? fc-total where
          fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
          fc-total with trio< ua ub
          ... | tri< a₁ ¬b ¬c with ≤-ftrans  (order (o<→≤ sub<x) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) a₁) fca ) (s≤fc (supf ub) f mf fcb )
@@ -466,24 +482,24 @@
       ft01 : (& a) ≤ (& b) → Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
          a=b : a ≡ b
-         a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
+         a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq)
       ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)  where
          a<b : a < b
-         a<b = subst₂ (λ j k → j < k ) *iso *iso lt
+         a<b = subst₂ (λ j k → j < k ) ? ? lt
       ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb))
    f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where
       ft01 : (& b) ≤ (& a) → Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b  (λ lt → ⊥-elim (<-irr (case1 a=b) lt))  where
          a=b : a ≡ b
-         a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq))
+         a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) (sym eq))
       ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where
          b<a : b < a
-         b<a = subst₂ (λ j k → j < k ) *iso *iso lt
+         b<a = subst₂ (λ j k → j < k ) ? ? lt
       ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
       ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
-      subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
+      subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ?  (fcn-cmp y f mf fca fcb )
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -505,7 +521,8 @@
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb )
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
-supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
+supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = ? where
+   -- Ordinals.inOrdinal.TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
        supfa = ZChain.supf za
        supfb = ZChain.supf zb
        ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
@@ -560,13 +577,13 @@
      z07 :   {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      s : HOD
-     s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
+     s = minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
      as : A ∋ * ( & s  )
-     as =  subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  )
+     as =  subst (λ k → odef A (& k) ) ? ( x∋minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  )
      as0 : odef A  (& s  )
      as0 =  subst (λ k → odef A k ) &iso as
      s<A : & s o< & A
-     s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as )
+     s<A = c<→o< (subst (λ k → odef A (& k) ) ? as )
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 }
      no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
@@ -575,7 +592,7 @@
      Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 }
      z08  : ¬ Maximal A →  HasMaximal =h= od∅
      z08 nmx  = record { eq→  = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; as = subst (λ k → odef A k) (sym &iso) (proj1 lt)
-         ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← =  λ {y} lt → ⊥-elim ( ¬x<0 lt )}
+         ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) ? (proj2 lt (& y) ay) } ) ; eq← =  λ {y} lt → ⊥-elim ( ¬x<0 lt )}
      x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
      x-is-maximal nmx {x} ax nogt m am  = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) ,  ¬x<m  ⟫ where
         ¬x<m :  ¬ (* x < * m)
@@ -590,15 +607,15 @@
          xsup sup = {w : Ordinal } → odef B w → (w ≡ sup ) ∨ (w << sup )
          ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
-         ∀-imply-or  {A} {B} ∀AB with ODC.p∨¬p O ((x : Ordinal ) → A x) -- LEM
+         ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
          ∀-imply-or  {A} {B} ∀AB | case1 t = case1 t
          ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x not )) where
                lemma : ¬ ((x : Ordinal ) → A x) →  B
-               lemma not with ODC.p∨¬p O B
+               lemma not with p∨¬p B
                lemma not | case1 b = b
                lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
          m00 : (x : Ordinal ) → ( ( z : Ordinal) → z o< x →  ¬ (odef A z ∧ xsup z) ) ∨ MinSUP A B
-         m00 x = TransFinite0 ind x where
+         m00 x = ? where -- Ordinals.inOrdinal.TransFinite0 ? x where
             ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( ( w : Ordinal) → w o< z →  ¬ (odef A w ∧ xsup w ))  ∨ MinSUP A B)
                   → ( ( w : Ordinal) → w o< x →  ¬ (odef A w ∧ xsup w) )  ∨ MinSUP A B
             ind x prev  =  ∀-imply-or m01 where
@@ -608,7 +625,7 @@
                 ... | tri> ¬a ¬b c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
                 ... | tri< a ¬b ¬c with prev z a
                 ... | case2 mins = case2 mins
-                ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z)
+                ... | case1 not with p∨¬p (odef A z ∧ xsup z)
                 ... | case1 mins = case2 record { sup = z ; isMinSUP = record { as = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where
                   m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1
                   m04 {s} as lt with trio< z s
@@ -630,18 +647,18 @@
 
      -- Uncountable ascending chain by axiom of choice
      cf : ¬ Maximal A → Ordinal → Ordinal
-     cf  nmx x with ODC.∋-p O A (* x)
+     cf  nmx x with ∋-p A (* x)
      ... | no _ = o∅
      ... | yes ax with is-o∅ (& ( Gtx ax ))
      ... | yes nogt = -- no larger element, so it is maximal
          ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
-     ... | no not =  & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
+     ... | no not =  & (minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
      is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) )
-     is-cf nmx {x} ax with ODC.∋-p O A (* x)
+     is-cf nmx {x} ax with ∋-p A (* x)
      ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax ))
      ... | yes ax with is-o∅ (& ( Gtx ax ))
      ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
-     ... | no not = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
+     ... | no not = x∋minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
 
      ---
      --- infintie ascention sequence of f
@@ -681,7 +698,7 @@
                   b o< x → (ab : odef A b) →
                   HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) b →
                   * a < * b → odef (UnionCF A f ay supf x) b
-               is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
+               is-max {a} {b} ua b<x ab P a<b with or-exclude P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
@@ -715,7 +732,7 @@
                   b o< x → (ab : odef A b) →
                   HasPrev A (UnionCF A f ay supf x) f b  ∨ IsSUP A (UnionCF A f ay supf b) b →
                   * a < * b → odef (UnionCF A f ay supf x) b
-               is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
+               is-max {a} {b} ua b<x ab P a<b with or-exclude P
                is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc  )
                ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay ,  ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
@@ -748,7 +765,7 @@
 
      utotal : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
         → IsTotalOrderSet (uchain f mf ay)
-     utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+     utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = fcn-cmp y f mf ca cb
 
@@ -821,18 +838,18 @@
           ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
           ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
                eq1 : a0 ≡ b0
-               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+               eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq )
           ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
                lt1 : a0 < b0
-               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+               lt1 = subst₂ (λ j k → j < k ) ? ? lt
           ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
           ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
                eq1 : a0 ≡ b0
-               eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+               eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq )
           ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
                lt1 : a0 < b0
-               lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-          ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b))
+               lt1 = subst₂ (λ j k → j < k ) ? ? lt
+          ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b))
 
           pcha : pchainpx ⊆ A
           pcha (case1 lt) = proj1 lt
@@ -1200,7 +1217,7 @@
       ptotalU : IsTotalOrderSet pchainU
       ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib))
       ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) ia<ib) (pchainU⊆chain ib)
-      ... | tri≈ ¬a ia=ib ¬c = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso ( pcmp (proj2 ia) (proj2 ib) ia=ib ) where
+      ... | tri≈ ¬a ia=ib ¬c = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? ( pcmp (proj2 ia) (proj2 ib) ia=ib ) where
            pcmp : (ia : IChain ay supfz (& a)) → (ib : IChain ay supfz (& b)) → IChain-i ia ≡ IChain-i ib
                → Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
            pcmp (ic-init fca) (ic-init fcb) eq = fcn-cmp _ f mf fca fcb
@@ -1232,7 +1249,7 @@
                fc12 = ftrans<-≤ lt (subst (λ k → k ≤ & a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) )
            pcmp (ic-isup i i<x s<x fca) (ic-isup i i<y s<y fcb) refl = fcn-cmp _ f mf fca (subst (λ k → FClosure A f k (& b)) pc01 fcb ) where
                pc01 : supfz i<y ≡ supfz i<x
-               pc01 = cong supfz  o<-irr
+               pc01 = ? -- cong supfz  o<-irr
       ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia)
 
 
@@ -1261,18 +1278,18 @@
       ptotalS {a0} {b0} (case1 a) (case2 b) with zc02 a b
       ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
            eq1 : a0 ≡ b0
-           eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+           eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq )
       ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
            lt1 : a0 < b0
-           lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+           lt1 = subst₂ (λ j k → j < k ) ? ? lt
       ptotalS {b0} {a0} (case2 b) (case1 a) with zc02 a b
       ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
            eq1 : a0 ≡ b0
-           eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+           eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq )
       ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
            lt1 : a0 < b0
-           lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
-      ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp spu0 f mf (proj1 a) (proj1 b))
+           lt1 = subst₂ (λ j k → j < k ) ? ? lt
+      ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp spu0 f mf (proj1 a) (proj1 b))
 
       S⊆A : pchainS ⊆ A
       S⊆A (case1 lt) = proj1 lt
@@ -1302,7 +1319,7 @@
 
           sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z
           sf1=sf {z} z<x with trio< z x
-          ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
+          ... | tri< a ¬b ¬c = ? -- cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
           ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
 
@@ -1576,20 +1593,20 @@
 
      zorn00 : Maximal A
      zorn00 with is-o∅ ( & HasMaximal )  
-     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where
+     ... | no not = record { maximal = minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where
          -- yes we have the maximal because of the axiom of choice 
-         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
-         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))   -- Axiom of choice
-         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
+         zorn03 :  odef HasMaximal ( & ( minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
+         zorn03 =  x∋minimal  HasMaximal  (λ eq → not (=od∅→≡o∅ eq))   -- Axiom of choice
+         zorn01 :  A ∋ minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq))
          zorn01  = proj1  zorn03
-         zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
-         zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
+         zorn02 : {x : HOD} → A ∋ x → ¬ (minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
+         zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) ? ? m<x )
      ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as0 (& A) )) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
-              zc5 = ⟪  Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
+              zc5 = ⟪  Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) ? mx<y) ) ⟫
 
 -- usage (see filter.agda )
 --