{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Ordinals
module ODC {n : Level } (O : Ordinals {n} ) where

open import zf
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
open import  Relation.Binary.PropositionalEquality
open import Data.Nat.Properties 
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

import OrdUtil
open import logic
open import nat
import OD
import ODUtil

open inOrdinal O
open OD O
open OD.OD
open OD._==_
open ODAxiom odAxiom
open ODUtil O

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O


open HOD

open _∧_

postulate      
  -- mimimul and x∋minimal is an Axiom of choice
  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
  -- minimality (proved by ε-induction with LEM)
  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )


--
-- Axiom of choice in intutionistic logic implies the exclude middle
--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
--

pred-od :  ( p : Set n )  → HOD
pred-od  p  = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc } 

ppp :  { p : Set n } { a : HOD  } → pred-od p ∋ a → p
ppp  {p} {a} d = proj2 d

p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
p∨¬p  p with is-o∅ ( & (pred-od p ))
p∨¬p  p | yes eq = case2 (¬p eq) where
   ps = pred-od p 
   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
   lemma : ps =h= od∅ → p → ⊥
   lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
   ¬p : (& ps ≡ o∅) → p → ⊥
   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
   ps = pred-od p 
   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
   lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))

decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
decp  p with p∨¬p p
decp  p | case1 x = yes x
decp  p | case2 x = no x

∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
∋-p A x with p∨¬p ( A ∋ x ) -- LEM
∋-p A x | case1 t  = yes t
∋-p A x | case2 t  = no (λ x → t x)

double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

open _⊆_

power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
   t1 = power→ A t PA∋t

power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01  where
   p01 :  {z : HOD} → (x ∩ y) ∋ z → A ∋ z
   p01 {z} xyz = double-neg-eilm (  power→ A x ax (proj1 xyz ))

OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
OrdP  x y with trio< x (& y)
OrdP  x y | tri< a ¬b ¬c = no ¬c
OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
OrdP  x y | tri> ¬a ¬b c = yes c

-- open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)

record Element (A : HOD) : Set (suc n) where
    field
       elm : HOD
       is-elm : A ∋ elm

open Element

TotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )  

PartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
PartialOrderSet A _<_ = (a b :  Element A)
     → (elm a < elm b → (¬ (elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))

me : { A a : HOD } → A ∋ a → Element A
me {A} {a} lt = record { elm = a ; is-elm = lt }

record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
   field
      sup : HOD
      A∋maximal : A ∋ sup
      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )

record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
   field
      maximal : HOD
      A∋maximal : A ∋ maximal
      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x

record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
   field
      B : HOD
      B⊆A : B ⊆ A 
      total : TotalOrderSet B _<_
      fb : {x : HOD } → A ∋ x  → HOD
      B∋fb : (x : HOD ) → (ax : A ∋ x)  → B ∋ fb ax
      ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< osuc y → sup < fb as

Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
    → o∅ o< & A 
    → ( {a b c : HOD} → a < b → b < c → a < c )
    → PartialOrderSet A _<_
    → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  )
    → Maximal A _<_ 
Zorn-lemma {A} {_<_} 0<A TR PO supP = zorn00 where
     someA : HOD
     someA = minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
     isSomeA : A ∋ someA
     isSomeA =  x∋minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
     HasMaximal : HOD
     HasMaximal = record { od = record { def = λ x → (m : Ordinal) →  odef A m → odef A x ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} } where
         z07 :  {y : Ordinal} → ((m : Ordinal) → odef A y ∧ odef A m ∧ (¬ (* y < * m))) → y o< & A
         z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 (p (& someA)) )))
     no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
     no-maximum nomx x P = ¬x<0 (eq→ nomx {x} (λ m am → P m am )) 
     Gtx : { x : HOD} → A ∋ x → HOD
     Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = {!!} } 
     z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = proj1 (proj2 (PO (me  A∋b) (me A∋a)) (sym a=b)) b<a
     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (PO (me  A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me  A∋b) (me A∋a)) b=a ) b<a ) ⟫
     ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
     ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z (SUP.A∋maximal sp)) (ZChain.B∋fb z  _ (SUP.A∋maximal sp)) (ZChain.¬x≤sup z _  (SUP.A∋maximal sp) z03 )) where
         z03 : & (SUP.sup sp) o< osuc (& A)
         z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
         z02 :  (x : HOD) → ZChain.B z ∋ x → SUP.sup sp < x → ⊥
         z02 x xe s<x = z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
     ind :  HasMaximal =h= od∅
         → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
         →  ZChain A x _<_
     ind nomx x prev with Oprev-p x
     ... | yes op with ∋-p A (* x)
     ... | no ¬Ax = record  { B = ZChain.B zc1 ; B⊆A =  ZChain.B⊆A  zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = z04 } where
          -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
          px = Oprev.oprev op
          zc1 : ZChain A px _<_
          zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
          z04 :  (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
          z04 sup as s<x with trio< (& sup) x
          ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
          ... | tri< a ¬b ¬c  = ZChain.¬x≤sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
          ... | tri> ¬a ¬b c with  osuc-≡< s<x
          ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )  
          ... | case2 lt = ⊥-elim (¬a lt )
     ... | yes ax = z06 where -- we have previous ordinal and A ∋ x
          px = Oprev.oprev op
          zc1 : ZChain A px _<_
          zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
          z06 : ZChain A x _<_
          z06 with is-o∅ (& (Gtx ax))
          ... | yes nogt = ⊥-elim (no-maximum nomx x x-is-maximal ) where -- no larger element, so it is maximal
              x-is-maximal :  (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
              x-is-maximal m am  = ⟪ subst (λ k → odef A k) &iso ax ,  ¬x<m  ⟫ where
                 ¬x<m :  ¬ (* x < * m)
                 ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
          ... | no not = record { B = Bx     --  we have larger element, let's create ZChain
              ; B⊆A = B⊆A ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
                 B = ZChain.B zc1 
                 Bx : HOD
                 Bx = record { od = record { def = λ y → (x ≡ y) ∨ odef B y } ; odmax = & A ; <odmax = {!!}  } 
                 B⊆A : Bx ⊆ A
                 B⊆A = record { incl = λ {y} by → z07 y by  } where
                     z07 : (y : HOD) → Bx ∋ y → A ∋ y
                     z07 y (case1 x=y) = subst (λ k → odef A k ) (trans &iso x=y) ax
                     z07 y (case2 by) = incl (ZChain.B⊆A zc1 ) by
                 m = minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
     ind nomx x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
     ... | tri< a ¬b ¬c = record { B = ZChain.B zc1
              ; B⊆A = ZChain.B⊆A zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = {!!} } where
          zc1 : ZChain A (& A) _<_
          zc1 = prev (& A) a 
     ... | tri≈ ¬a b ¬c = record { B = B
              ; B⊆A = {!!} ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
          B : HOD
          B = record { od = record { def = λ y → (y<x : y o< x ) → odef (ZChain.B (prev y y<x)) y } ; odmax = & A ; <odmax = {!!} } 
     ... | tri> ¬a ¬b c = {!!}
     zorn00 : Maximal A _<_
     zorn00 with is-o∅ ( & HasMaximal )
     ... | no not = record { maximal = minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
         zorn03 :  odef HasMaximal ( & ( minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
         zorn03 =  x∋minimal  HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
         zorn01 :  A ∋ minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq))
         zorn01 =  proj1 (zorn03 (& someA) isSomeA ) 
         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) (sym *iso) (sym *iso) m<x )
     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A) (≡o∅→=od∅ ¬Maximal)) ( supP B (ZChain.B⊆A (z (& A) (≡o∅→=od∅ ¬Maximal))) (ZChain.total (z (& A) (≡o∅→=od∅ ¬Maximal))) )) where
         z : (x : Ordinal) → HasMaximal =h= od∅  → ZChain A x _<_ 
         z x nomx = TransFinite (ind nomx) x
         B = ZChain.B (z (& A) (≡o∅→=od∅ ¬Maximal)  )

open import zfc

HOD→ZFC : ZFC
HOD→ZFC   = record { 
    ZFSet = HOD 
    ; _∋_ = _∋_ 
    ; _≈_ = _=h=_ 
    ; ∅  = od∅
    ; Select = Select
    ; isZFC = isZFC
 } where
    -- infixr  200 _∈_
    -- infixr  230 _∩_ _∪_
    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
    isZFC = record {
       choice-func = choice-func ;
       choice = choice
     } where
         -- Axiom of choice ( is equivalent to the existence of minimal in our case )
         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
         choice-func X {x} not X∋x = minimal x not
         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 
         choice X {A} X∋A not = x∋minimal A not