# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719713013 -32400
# Node ID ba406e2ba8af6d519b35b713882e91523ff18e7f
# Parent  22523e8af390d062356a3c57a5d4bcabd215d95d
...

diff -r 22523e8af390 -r ba406e2ba8af src/zorn.agda
--- a/src/zorn.agda	Sun Jun 30 06:44:27 2024 +0900
+++ b/src/zorn.agda	Sun Jun 30 11:03:33 2024 +0900
@@ -13,7 +13,10 @@
 
 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
+        (_<_ : (x y : OD.HOD O HODAxiom) → Set n ) 
+        (<-cong : {x y w z : OD.HOD O HODAxiom} 
+            → HODBase._==_ O (HODBase.HOD.od x) (HODBase.HOD.od w) → HODBase._==_ O (HODBase.HOD.od  y) (HODBase.HOD.od z) → x < y  → w < z )
+        (PO : IsStrictPartialOrder _≡_ _<_ ) where
 
 
 -- open import  Relation.Binary.Structures
@@ -21,6 +24,7 @@
 open import Data.Nat hiding ( _≤_  ; _<_ )
 
 import OrdUtil
+open inOrdinal O
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
@@ -90,8 +94,8 @@
 ftrans<-≤ {x} {y} {z} x<y (case1 eq) = subst (λ k → * x < k ) ((cong (*) eq)) x<y
 ftrans<-≤ {x} {y} {z} x<y (case2 lt) = IsStrictPartialOrder.trans PO x<y lt
 
-<-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
+<-irr : {a b : Ordinal} → (a ≡ b ) ∨ (* a < * b ) → * b < * a → ⊥
+<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym (cong (*) a=b) ) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
           (IsStrictPartialOrder.trans PO     b<a a<b)
 
@@ -147,46 +151,45 @@
 ... | case2 y<fy = suc (fcn s mf p )
 
 fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
-     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
+     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → x ≡ y
 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
      fc06 : {y : Ordinal } { as : odef A s } (eq : s ≡ y  ) { j : ℕ } →  ¬ suc j ≡ fcn {A} s {y} {f} mf (init as eq )
      fc06 {x} {y} refl {j} not = fc08 not where
         fc08 :  {j : ℕ} → ¬ suc j ≡ 0
         fc08 ()
-     fc07 : {x : Ordinal } (cx : FClosure A f s x ) → 0 ≡ fcn s mf cx → * s ≡ * x
+     fc07 : {x : Ordinal } (cx : FClosure A f s x ) → 0 ≡ fcn s mf cx → s ≡ x
      fc07 {x} (init as refl) eq = refl
      fc07 {.(f x)} (fsuc x cx) eq with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → * s ≡  k ) (cong (*) x=fx) ( fc07 cx eq )
-     -- ... | case2 x<fx = ?
-     fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
+     ... | case1 x=fx = trans (fc07 cx eq ) x=fx
+     fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → x ≡ y
      fc00 (suc i) (suc j) x cx (init x₃ x₄) x₁ x₂ = ⊥-elim ( fc06 x₄ x₂ )
      fc00 (suc i) (suc j) x (init x₃ x₄) (fsuc x₅ cy) x₁ x₂ = ⊥-elim ( fc06 x₄ x₁ )
      fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl
      fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * s ≡ * k ) y=fy (fc07 cy i=y) -- ( fc00 zero zero refl (init as refl) cy i=x i=y )
+     ... | case1 y=fy = trans (fc07 cy i=y) y=fy 
      fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → * k ≡ * s ) x=fx (sym (fc07 cx i=x)) -- ( fc00 zero zero refl cx (init as refl) i=x i=y )
+     ... | case1 x=fx = sym (trans (fc07 cx i=x) x=fx ) 
      fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → * j ≡ * k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
+     ... | case1 x=fx  | case1 y=fy = trans (sym x=fx) (trans ( fc00 zero zero refl cx cy  i=x i=y ) y=fy)
      fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → * j ≡ * k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy  i=x j=y )
-     ... | case1 x=fx | case2 y<fy = subst (λ k → * k ≡ * (f y)) x=fx (fc02 x cx i=x) where
-          fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y)
+     ... | case1 x=fx | case1 y=fy = trans (sym x=fx) (trans ( fc00 (suc i) (suc j) i=j cx cy  i=x j=y ) y=fy )
+     ... | case1 x=fx | case2 y<fy = trans (sym x=fx) (fc02 x cx i=x) where
+          fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → x1 ≡ f y
           fc02 x1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x)
           fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) )
-          ... | case1 eq = trans (sym (cong (*) eq )) ( fc02  x1 cx1 i=x1 )  -- derefence while f x ≡ x
-          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where
-               fc04 : * x1 ≡ * y
+          ... | case1 eq = trans (sym eq ) ( fc02  x1 cx1 i=x1 )  -- derefence while f x ≡ x
+          ... | case2 lt = cong f fc04  where
+               fc04 : x1 ≡ y
                fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
-     ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ * k ) y=fy (fc03 y cy j=y) where
-          fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
+     ... | case2 x<fx | case1 y=fy = trans (fc03 y cy j=y) y=fy where
+          fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → f x  ≡ y1
           fc03 y1 (init x₁ x₂) x = ⊥-elim (fc06 x₂ x)
           fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
-          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) (cong (*) eq)
-          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
-               fc05 : * x ≡ * y1
+          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) eq
+          ... | case2 lt = cong f fc05 where 
+               fc05 : x ≡ y1
                fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
-     ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y)))
+     ... | case2 x₁ | case2 x₂ = cong f  (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y))
 
 
 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
@@ -202,7 +205,7 @@
      ... | case1 y=fy = subst (λ k → * x < k ) (cong (*) y=fy) ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i)  )
      ... | case2 y<fy with <-cmp (fcn s mf cx ) i
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i c )
-     ... | tri≈ ¬a b ¬c = subst (λ k → k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy
+     ... | tri≈ ¬a b ¬c = subst (λ k → * k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy
      ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO fc02 y<fy where
           fc03 :  suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy
           fc03 eq = cong pred eq
@@ -211,13 +214,13 @@
 
 
 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f)
-    → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
+    → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (x ≡ y) (* y < * x )
 fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy )
 ... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
       fc11 : * x < * y
       fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a
 ... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where
-      fc10 : * x ≡ * y
+      fc10 : x ≡ y
       fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b
 ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12  where
       fc12 : * y < * x
@@ -271,7 +274,7 @@
     → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
 fc-stop A f mf {a} {b} aa x≤sup a=b with x≤sup (fsuc a (init aa refl ))
 ... | case1 eq = trans eq (sym a=b)
-... | case2 lt = ⊥-elim (<-irr (case1 (cong (λ k → * (f k) ) (sym a=b))) (ftrans<-≤ lt fc00 ) ) where
+... | case2 lt = ⊥-elim (<-irr (case1 (cong f (sym a=b))) (ftrans<-≤ lt fc00 ) ) where
      fc00 :   b ≤  (f b)
      fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
 
@@ -463,43 +466,29 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
 
    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)) ? ? fc-total where
+   f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = 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 )
-         ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ?)) lt)) ?  (λ lt → ⊥-elim (<-irr (case1 ?) lt)) where
-                  ct00 : a ≡ b
-                  ct00 = ?
-         ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 ?) a<b ) (λ lt → <-irr (case2 a<b ) lt)
+         ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym eq1)) lt)) eq1  (λ lt → ⊥-elim (<-irr (case1 eq1) lt)) 
+         ... | case2 a<b =  tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt)
          fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb
          fc-total | tri> ¬a ¬b c with ≤-ftrans  (order (o<→≤ sua<x) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) c) fcb ) (s≤fc (supf ua) f mf fca )
-         ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ?)) lt)) ?  (λ lt → ⊥-elim (<-irr (case1 ?) lt)) where
-                  ct00 : a ≡ b
-                  ct00 = ?
+         ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 eq1) lt)) (sym eq1)  (λ lt → ⊥-elim (<-irr (case1 (sym eq1)) lt)) 
          ... | case2 b<a =  tri> (λ lt → <-irr (case2 b<a ) lt)  (λ eq → <-irr (case1 eq) b<a )  b<a
    f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where
       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 ) ? ? (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 ) ? ? lt
+      ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym eq)) lt)) eq  (λ lt → ⊥-elim (<-irr (case1 eq) lt))  
+      ft01 (case2 a<b) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) 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 ) ? ? (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 ) ? ? lt
+      ft01 : b ≤ a → Tri ( * a <  * b) ( a ≡  b) ( * b <  * a )
+      ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 eq) lt)) (sym eq) (λ lt → ⊥-elim (<-irr (case1 (sym eq)) lt))  
+      ft01 (case2 b<a) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a 
       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)) ? ?  (fcn-cmp y f mf fca fcb )
+   f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = 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
@@ -521,8 +510,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 = ? where
-   -- Ordinals.inOrdinal.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 = 
+  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
@@ -571,19 +560,15 @@
     → o∅ o< & A
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A
-Zorn-lemma {A}  0<A supP = zorn00 where
-     <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-     <-irr0 {a} {b} A∋a A∋b = <-irr
+Zorn-lemma {A}  0<A supP = ? where
      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 = minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
-     as : A ∋ * ( & s  )
-     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
+     as : A ∋ s
+     as =  x∋minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  
      s<A : & s o< & A
-     s<A = c<→o< (subst (λ k → odef A (& k) ) ? as )
+     s<A = c<→o< 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) )) →  ⊥
@@ -592,7 +577,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)) ? (proj2 lt (& y) ay) } ) ; eq← =  λ {y} lt → ⊥-elim ( ¬x<0 lt )}
+         ; ¬maximal<x = λ {y} ay x<y → proj2 lt (& y) ay (<-cong ==-refl (==-sym *iso) x<y) } ) ; 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)
@@ -615,7 +600,7 @@
                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 = ? where -- Ordinals.inOrdinal.TransFinite0 ? x where
+         m00 x = TransFinite0 ind 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
@@ -708,7 +693,7 @@
                   m05 =  ZChain.sup=u zc ab (o<→≤ (odef< ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
-               ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
+               ... | case1 sb=sx = ⊥-elim (<-irr (case1 m10) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17
@@ -744,7 +729,7 @@
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) record { ax = ab ; x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt }
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
-               ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
+               ... | case1 sb=sx = ⊥-elim (<-irr (case1 m10) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17
@@ -765,9 +750,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)) ? ? uz01 where
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = fcn-cmp y f mf ca cb
+     utotal f mf {y} ay {a} {b} ca cb = fcn-cmp y f mf ca cb
 
      ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
        →  MinSUP A (uchain f mf ay)
@@ -836,20 +819,12 @@
           ptotal : IsTotalOrderSet pchainpx
           ptotal (case1 a) (case1 b) =  ZChain.f-total zc a b
           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 ) ? ? (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 ) ? ? lt
+          ... | case1 eq = tri≈ (<-irr (case1 (sym eq))) eq (<-irr (case1 eq)) 
+          ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (<-irr (case2 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 ) ? ? (cong (*) eq )
-          ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
-               lt1 : a0 < b0
-               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))
+          ... | case1 eq = tri≈ (<-irr (case1 eq)) (sym eq) (<-irr (case1 (sym eq))) 
+          ... | case2 lt = tri> (<-irr (case2 lt)) (λ eq → <-irr (case1 eq) lt) lt  
+          ptotal (case2 a) (case2 b) = fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b)
 
           pcha : pchainpx ⊆ A
           pcha (case1 lt) = proj1 lt
@@ -1217,39 +1192,39 @@
       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)) ? ? ( 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) )
+      ... | tri≈ ¬a ia=ib ¬c = 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
            pcmp (ic-init fca) (ic-isup i i<x s<x fcb) eq with ZChain.fcy<sup (pzc i<x) o≤-refl fca
            ... | case1 eq1 = ct22 where
-               ct22 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               ct22 with subst (λ k → k ≤ & b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb )
+               ct22 : Tri (* a < * b) (a ≡ b) (* b < * a )
+               ct22 with subst (λ k → k ≤ b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb )
                ... | case1 eq2 =  tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-                   ct00 : * (& a) ≡ * (& b)
-                   ct00 = cong (*) (trans eq1 eq2)
+                   ct00 : a ≡ b
+                   ct00 = trans eq1 eq2
                ... | case2 lt = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
-                   fc11 : * (& a) < * (& b)
-                   fc11 = subst (λ k →  k < * (& b) ) (cong (*) (sym eq1)) lt
+                   fc11 : * a < * b
+                   fc11 = subst (λ k →  k < * b ) (cong (*) (sym eq1)) lt
            ... | case2 lt = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
-               fc11 : * (& a) < * (& b)
-               fc11 = ftrans<-≤ lt (subst (λ k → k ≤ & b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb ) )
+               fc11 : * a < * b
+               fc11 = ftrans<-≤ lt (subst (λ k → k ≤ b) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fcb ) )
            pcmp (ic-isup i i<x s<x fca) (ic-init fcb) eq with ZChain.fcy<sup (pzc i<x) o≤-refl fcb
            ... | case1 eq1 =  ct22 where
-               ct22 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               ct22 with subst (λ k → k ≤ & a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca )
+               ct22 : Tri (* a < * b) (a ≡ b) (* b < * a )
+               ct22 with subst (λ k → k ≤ a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca )
                ... | case1 eq2 =  tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-                   ct00 : * (& a) ≡ * (& b)
-                   ct00 = cong (*) (sym (trans eq1 eq2))
+                   ct00 : a ≡ b
+                   ct00 = sym (trans eq1 eq2)
                ... | case2 lt = tri> (λ lt → <-irr (case2 fc11) lt) (λ eq → <-irr (case1 eq) fc11) fc11  where
-                   fc11 : * (& b) < * (& a)
-                   fc11 = subst (λ k →  k < * (& a) ) (cong (*) (sym eq1)) lt
+                   fc11 : * b < * a
+                   fc11 = subst (λ k →  k < * a ) (cong (*) (sym eq1)) lt
            ... | case2 lt = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12  where
-               fc12 : * (& b) < * (& a)
-               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
+               fc12 : * b < * a
+               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 = zeq ? ? ? ?
       ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia)
 
 
@@ -1276,20 +1251,12 @@
       ptotalS : IsTotalOrderSet pchainS
       ptotalS (case1 a) (case1 b) =  ptotalU a b
       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 ) ? ? (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 ) ? ? lt
+      ... | case1 eq = tri≈ (<-irr (case1 (sym eq))) eq (<-irr (case1 eq)) 
+      ... | case2 lt = tri< lt (λ eq → <-irr (case1 (sym eq)) lt) (<-irr (case2 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 ) ? ? (cong (*) eq )
-      ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
-           lt1 : a0 < b0
-           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))
+      ... | case1 eq = tri≈ (<-irr (case1 eq)) (sym eq) (<-irr (case1 (sym eq))) 
+      ... | case2 lt = tri> (<-irr (case2 lt)) (λ eq → <-irr (case1 eq) lt) lt  
+      ptotalS (case2 a) (case2 b) = fcn-cmp spu0 f mf (proj1 a) (proj1 b)
 
       S⊆A : pchainS ⊆ A
       S⊆A (case1 lt) = proj1 lt
@@ -1524,7 +1491,7 @@
      -- f eventualy stop
      --    we can prove contradict here, it is here for a historical reason
      --
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf< as0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf< as (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
      fixpoint f mf mf< zc sp1 = z14 where
@@ -1534,17 +1501,17 @@
            sp = MinSUP.sup sp1
            asp : odef A sp
            asp = MinSUP.as sp1
-           ay = as0
+           ay = as
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f ay (ZChain.supf zc) b) b
               → * a < * b  → odef chain b
-           z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
+           z10 = ZChain1.is-max (SZ1 f mf mf< as zc (& A) o≤-refl )
            z22 : sp o< & A
            z22 = odef< asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (odef< asp) asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (odef< asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
@@ -1553,7 +1520,7 @@
                z19 = record { ax = asp ;   x≤sup = z20 }  where
                    z20 : {y : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
                    z20 {y} zy with MinSUP.x≤sup sp1
-                       (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as0 supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
+                       (subst (λ k → odef chain k ) (sym &iso) (chain-mono f mf as supf (ZChain.supf-mono zc) (o<→≤ z22)  zy ))
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso y=p )
                    ... | case2 y<p = case2 (subst (λ k → * k < _ ) &iso y<p )
            z14 :  f sp ≡ sp
@@ -1561,16 +1528,16 @@
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.as sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (sym (cong (*) eq ) ))
-               ... | case2 lt = ⊥-elim (¬c lt )
-           ... | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b )
+               ... | case1 eq = ⊥-elim (¬b (sym ? ))
+               ... | case2 lt = ⊥-elim (¬c ? )
+           ... | tri≈ ¬a b ¬c = ? -- subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) )
                z15  = MinSUP.x≤sup sp1 (ZChain.f-next zc z12 )
                z17 : ⊥
                z17 with z15
-               ... | case1 eq = ¬b (cong (*) eq)
-               ... | case2 lt = ¬a lt
+               ... | case1 eq = ¬b ?
+               ... | case2 lt = ¬a ?
 
      -- ZChain contradicts ¬ Maximal
      --
@@ -1578,16 +1545,16 @@
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
 
-     ¬Maximal→¬cf-mono :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-<-monotonic nmx) as0 (& A)) → ⊥
-     ¬Maximal→¬cf-mono nmx zc = <-irr0  {* (cf nmx c)} {* c}
-           (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
-           (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
-                (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1 ))) where          -- x < f x
-
+     ¬Maximal→¬cf-mono :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-<-monotonic nmx) as (& A)) → ⊥
+     ¬Maximal→¬cf-mono nmx zc = <-irr  {cf nmx c} {c}
+           ? -- (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
+           ? -- (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
+           -- (case1 ( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1 ) -- x ≡ f x ̄
+           --     (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1))))  where          -- x < f x
+             where
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)
-          msp1 = msp0 (cf nmx) (cf-is-<-monotonic nmx) as0 zc
+          msp1 = msp0 (cf nmx) (cf-is-<-monotonic nmx) as zc
           c : Ordinal
           c = MinSUP.sup msp1
 
@@ -1601,7 +1568,7 @@
          zorn01  = proj1  zorn03
          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
+     ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as (& A) )) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
@@ -1626,3 +1593,4 @@
 --        → Maximal P (_⊆_)
 -- MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆_} 0<P PO SP
 --
+