{-# OPTIONS --allow-unsolved-metas #-}
open import Level hiding ( suc ; zero )
open import Ordinals
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import OD hiding ( _⊆_ )
module zorn1 {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where

--
-- Zorn-lemma : { A : HOD }
--     → o∅ o< & A
--     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
--     → Maximal A
--

open import zf -- hiding ( _⊆_ )
open import logic
-- open import partfunc {n} O

open import Relation.Nullary
open import Data.Empty
import BAlgbra

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 )
--

_<<_ : (x y : Ordinal ) → Set n
x << y = * x < * y

_≤_ : (x y : Ordinal ) → Set n    -- we can't use * x ≡ * y, it is Set (Level.suc n). Level (suc n) troubles Chain
x ≤ y = (x ≡ y ) ∨ ( * x < * y )

POO : IsStrictPartialOrder _≡_ _<<_
POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
   ; trans = IsStrictPartialOrder.trans PO
   ; irrefl = λ x=y x<y → IsStrictPartialOrder.irrefl PO (cong (*) x=y) x<y
   ; <-resp-≈ =  record { fst = λ {x} {y} {y1} y=y1 xy1 → subst (λ k → x << k ) y=y1 xy1 ; snd = λ {x} {x1} {y} x=x1 x1y → subst (λ k → k << x ) x=x1 x1y } }

≤-ftrans : {x y z : Ordinal } →  x ≤  y →  y ≤  z →  x ≤  z
≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )

ftrans≤-< : {x y z : Ordinal } →  x ≤  y →  y << z →  x <<  z
ftrans≤-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
ftrans≤-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z

ftrans<-≤ : {x y z : Ordinal } →  x <<  y →  y ≤ z →  x <<  z
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} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
          (IsStrictPartialOrder.trans PO     b<a a<b)

<<-irr : {a b : Ordinal } → a ≤ b  → b << a → ⊥
<<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (cong (*) (sym a=b)) b<a
<<-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO refl (IsStrictPartialOrder.trans PO b<a a<b)

ptrans =  IsStrictPartialOrder.trans PO

open _==_
-- open _⊆_ -- we use different definition

-- We cannot prove this without Well foundedness of A
--
-- <-TransFinite : {A x : HOD} → {P : HOD → Set n} → x ∈ A
--     → ({y : HOD} → A ∋  y → y < x → P y ) → P x
-- <-TransFinite = ?

--
-- Closure of ≤-monotonic function f has total order
--

≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n
≤-monotonic-f A f = (x : Ordinal ) → odef A x → (  x ≤  (f x) ) ∧  odef A (f x )

<-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n
<-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x < * (f x) ) ∧  odef A (f x )

IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )

_⊆_ : ( A B : HOD ) → Set n
_⊆_ A B = {x : Ordinal } → odef A x → odef B x

⊆-IsTotalOrderSet : { A B : HOD } →  B ⊆ A  → IsTotalOrderSet A → IsTotalOrderSet B
⊆-IsTotalOrderSet {A} {B} B⊆A T  ax ay = T (B⊆A ax) (B⊆A ay)

record HasPrev (A B : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal )   : Set n where
   field
      ax : odef A x
      y : Ordinal
      ay : odef B y
      x=fy :  x ≡ f y

record IsSUP (A B : HOD) (x : Ordinal ) : Set n where
   field
      ax : odef A x
      x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -- B is Total, use positive

record SUP ( A B : HOD )  : Set (Level.suc n) where
   field
      sup : HOD
      isSUP : IsSUP A B (& sup)
   ax = IsSUP.ax isSUP
   x≤sup = IsSUP.x≤sup isSUP

record IsMinSUP ( A B : HOD ) (sup : Ordinal) : Set n where
   field
      as : odef A sup
      x≤sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )
      minsup : { sup1 : Ordinal } → odef A sup1
         →  ( {x : Ordinal  } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 ))  → sup o≤ sup1

record MinSUP ( A B : HOD )  : Set n where
   field
      sup : Ordinal
      isMinSUP : IsMinSUP A B sup
   as = IsMinSUP.as isMinSUP
   x≤sup = IsMinSUP.x≤sup isMinSUP
   minsup = IsMinSUP.minsup isMinSUP

record IChain (A : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal ) : Set n where
   field
      y : Ordinal
      x=fy   : x ≡ f y

z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))

--
--   Our Proof strategy of the Zorn Lemma  
--
--         f (f ( ... (supf y))) f (f ( ... (supf z1)))
--        /          |         /             |
--       /           |        /              |
--    supf y   <       supf z1          <    supf z2
--           o<                      o<
--
--    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
--    this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal.
--


∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))

-- Union of supf z and FClosure A f y

record Maximal ( A : HOD )  : Set (Level.suc n) where
   field
      maximal : HOD
      as : A ∋ maximal
      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative

Zorn-lemma : { A : HOD }
    → 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
     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 ))
     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 ))  )
     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 )
     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) )) →  ⊥
     no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ⟪ proj1 P , (λ m ma p → proj2 ( proj2 P m ma ) p ) ⟫ )
     Gtx : { x : HOD} → A ∋ x → HOD
     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 )}
     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)
        ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt)

     --
     -- we have minsup using LEM, this is similar to the proof of the axiom of choice
     --
     minsupP :  ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → MinSUP A B
     minsupP B B⊆A total = m02 where
         xsup : (sup : Ordinal ) → Set n
         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 | 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 | 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
            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
                m01 : (z : Ordinal) → (z o< x → ¬ (odef A z ∧ xsup z)) ∨ MinSUP A B
                m01 z with trio< z x
                ... | tri≈ ¬a b ¬c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
                ... | 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 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
                  ... | tri< a ¬b ¬c = o<→≤ a
                  ... | tri≈ ¬a b ¬c = o≤-refl0 b
                  ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫  )
                ... | case2 notz = case1 (λ _ → notz )
         m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z)
         m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
             S : SUP A B
             S = supP B  B⊆A total
             s1 = & (SUP.sup S)
             m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 )
             m05 {w} bw with SUP.x≤sup S bw
             ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq))
             ... | case2 lt = case2 lt
         m02 : MinSUP A B
         m02 = dont-or (m00 (& A)) m03

--   -- Uncountable ascending chain by axiom of choice
--   cf : ¬ Maximal A → Ordinal → Ordinal
--   cf  nmx x with ODC.∋-p O 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)))
--   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)
--   ... | 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))
--
--   ---
--   --- infintie ascention sequence of f
--   ---
--   cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
--   cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
--   cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
--   cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫

     ---
     --- the maximum chain  has fix point of any ≤-monotonic function
     ---

     record ZChain ( A : HOD ) {y : Ordinal} (ay : odef A y) (x : Ordinal) : Set (Level.suc n) where
       field
          chain : HOD
          chain⊆A : chain ⊆ A
          f-total  : IsTotalOrderSet chain
          cf : Ordinal → Ordinal 
          is-cf : {x : Ordinal} → odef A x → odef A (cf x) ∧ ( * x < * (cf x) )
          f-next  : {x : Ordinal } → odef chain x → odef chain (cf x)
          fixpoint : (sp1 : MinSUP A chain ) → odef chain (MinSUP.sup sp1)
       cf-is-<-monotonic : <-monotonic-f A cf
       cf-is-<-monotonic x ax = ⟪ proj2 (is-cf ax ) , proj1 (is-cf ax ) ⟫
       cf-is-≤-monotonic : ≤-monotonic-f A cf 
       cf-is-≤-monotonic x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic x ax  ))  , proj2 ( cf-is-<-monotonic x ax  ) ⟫

     SZ : ¬ Maximal A → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A ay x
     SZ nmx  {y} ay x =  TransFinite {λ z → ZChain A ay z  } (λ x → ind x ) x where
          ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ZChain A ay z) → ZChain A ay x
          ind x prev = ?  -- with Oprev-p x

--  record {
--       chain = record { od = record { def = λ x → odef A x ∧ IChain A f x } ; odmax = & A ; <odmax = λ lt → z09 (proj1 lt) } ;
--       chain⊆A = λ cx → proj1 cx ;
--       f-total = λ ia ib → subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (f-total (proj2 ia) (proj2 ib))  ; 
--       f-next = λ ix → ⟪ ? , f-next (proj2 ix) ⟫ ;
--       fixpoint = λ sp1 → ⟪ ? , ? ⟫
--    } where
--       f-total : {a b : Ordinal } → IChain A f a → IChain A f b → Tri (a << b) (* a ≡ * b) (b << a) 
--       f-total = ?
--       f-next : {a : Ordinal } → IChain A f a → IChain A f (f a) 
--       f-next record { y = y ; x=fy = x=fy } = record { y = f y ; x=fy = cong f x=fy }

     msp0 : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
         → (zc : ZChain A ay (& A) )
         → MinSUP A (ZChain.chain zc) 
     msp0 f mf< {x} ay zc = minsupP (ZChain.chain zc)  (ZChain.chain⊆A zc) (ZChain.f-total zc)

     -- f eventualy stop
     --    we can prove contradict here, it is here for a historical reason
     --
     fixpoint : (zc : ZChain A  as0 (& A))
            → (sp1 : MinSUP A (ZChain.chain zc))
            → ZChain.cf zc (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
     fixpoint zc sp1 = z14 where
           chain = ZChain.chain zc
           sp : Ordinal
           sp = MinSUP.sup sp1
           asp : odef A sp
           asp = MinSUP.as sp1
           f = ZChain.cf zc
           mf : ≤-monotonic-f A f
           mf = ZChain.cf-is-≤-monotonic zc
           z12 : odef chain sp
           z12 = ZChain.fixpoint zc sp1
           z14 :  f sp ≡ sp
           z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 )
           ... | 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 )
           ... | 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

     -- ZChain contradicts ¬ Maximal
     --
     -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
     -- ¬ 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 as0 (& A)) → ⊥
     ¬Maximal→¬cf-mono nmx zc = <-irr0  {* (ZChain.cf zc c)} {* c}
           (subst (λ k → odef A k ) (sym &iso) (proj1 (ZChain.is-cf zc (MinSUP.as  msp1 ))))
           (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
           (case1 ( cong (*)( fixpoint zc msp1  ))) -- x ≡ f x ̄
                (proj1 (ZChain.cf-is-<-monotonic zc c (MinSUP.as msp1 ))) where          -- x < f x

          msp1 : MinSUP A (ZChain.chain zc)
          msp1 = msp0 (ZChain.cf zc) (ZChain.cf-is-<-monotonic zc) as0 zc
          c : Ordinal
          c = MinSUP.sup msp1

     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
         -- 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))
         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 )
     ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ 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) ) ⟫

-- usage (see filter.agda )
--
--  import OD hiding ( _⊆_ )
-- _⊆_ : ( A B : HOD ) → Set n
-- _⊆_ A B = {x : Ordinal } → odef A x → odef B x
-- 
-- import zorn 
-- open zorn O _⊆_   -- Zorn on Set inclusion order 
-- 
-- open import  Relation.Binary.Structures

-- MaximumSubset : {L P : HOD}
--        → o∅ o< & L →  o∅ o< & P → P ⊆ L
--        → IsPartialOrderSet P _⊆_
--        → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆_ → SUP P B _⊆_ )
--        → Maximal P (_⊆_)
-- MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆_} 0<P PO SP
--