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

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

-- elm-cmp : {A a b : HOD} → {_<_ : (x y : HOD) → Set n }  → A ∋ a →  A ∋ b →  TotalOrderSet A _<_  → Tri _ _ _
-- elm-cmp {A} {a} {b} ax bx cmp = cmp (me ax) (me bx)

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 : HOD
      ¬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< y → sup < fb as

Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
    → o∅ o< & A 
    → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  )
    → Maximal A _<_ 
Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
     HasMaximal : HOD
     HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
     z01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
     z01 {B} {a} {b} Tri  B∋a  B∋b (case1 a=b) b<a with Tri (me  B∋a) (me B∋b) 
     ... | tri< a₁ ¬b ¬c = ¬b  a=b
     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
     ... | tri> ¬a ¬b c = ¬b a=b
     z01 {B} {a} {b} Tri  B∋a  B∋b (case2 a<b) b<a with Tri (me  B∋a) (me B∋b) 
     ... | tri< a₁ ¬b ¬c = ¬c b<a
     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
     ... | tri> ¬a ¬b c = ¬a a<b
     ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
     ZChain→¬SUP z sp = ⊥-elim {!!} where
         z02 :  (x : HOD) → ZChain.B z ∋ x → ⊥
         z02 x xe = ( z01 (ZChain.total z) xe {!!} (SUP.x≤sup sp xe) {!!} )
     ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
         →  ZChain A x _<_
     ind x prev with Oprev-p x
     ... | yes _ = {!!}
     ind x prev | no ¬ox with trio< (& A) x
     ... | tri< a ¬b ¬c = {!!}
     ... | tri≈ ¬a b ¬c = {!!}
     ... | 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 = {!!}; ¬maximal<x  = {!!} }
     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP B (ZChain.B⊆A (z (& A))) (ZChain.total (z (& A)))) ) where
         z : (x : Ordinal) → ZChain A x _<_ 
         z = TransFinite ind 
         B = ZChain.B (z (& A))

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