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

open import zf
open import logic
open _∧_
open _∨_
open Bool

import OD
open import Relation.Nullary
open import Data.Empty
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
import BAlgebra
open BAlgebra O
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 import filter O
open import OPair O
open import Topology O
-- open import maximum-filter O

open Filter  
open Topology 

-- FIP is UFL

-- filter Base
record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
   field
       b x : Ordinal
       b⊆X : * b ⊆ * X
       sb  : Subbase (* b) x
       u⊆P : * u ⊆ P
       x⊆u : * x ⊆ * u

record UFLP {P : HOD} (TP : Topology P)  (F : Filter {Power P} {P} (λ x → x) )
       (ultra : ultra-filter F ) : Set (suc (suc n)) where
   field
       limit : Ordinal
       P∋limit : odef P limit
       is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F

UFLP→FIP : {P : HOD} (TP : Topology P) →
   ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
UFLP→FIP {P} TP uflp with trio< (& P) o∅
... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where
   -- P is empty
   fip02 : {x : Ordinal } → ¬ odef P x
   fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) )
   fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} →
            odef (* X) x → odef (* x) o∅
   -- empty P case
   --   if 0 < X then 0 < x ∧ P ∋ xfrom fip
   --   if 0 ≡ X then ¬ odef X x
   fip03 {X} CX fip {x} xx with trio< o∅ X
   ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso)
        ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe ))) where
      0<x : o∅ o< x
      0<x = fip (gi xx )
      e : HOD  -- we have an element of x
      e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
      xe : odef (* x) (& e)
      xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
   ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
           * X ≡⟨ cong (*) (sym 0=X) ⟩
           * o∅ ≡⟨  o∅≡od∅ ⟩
           od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
   ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  uf01 } where
     fip : {X : Ordinal} → * X ⊆ CS TP → Set n
     fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
     N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
     N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
        ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt))  }
     N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
     N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
     -- filter base is not empty
     nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
     nc {X} 0<X CSX fip = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where
          e : HOD  -- we have an element of X
          e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
          Xe : odef (* X) (& e)
          Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
     N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) 
        → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
     N∋nc {X} 0<X CSX fip = record { b = ? ; x =  ? ;  b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where
          e : HOD  -- we have an element of X
          e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
          Xe : odef (* X) (& e)
          Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
          nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) 
     0<PP : o∅ o< & (Power P)
     0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
          nn00 : odef (Power P) o∅
          nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt
          ... | x<0 = ⊥-elim ( ¬x<0 x<0)
     --
     -- FIP defines a filter
     --
     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
         f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
              f10 : q ⊆ P
              f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
              p∩q⊆p : * (& (p ∩ q)) ⊆ P
              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
              Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
              xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
              sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
              f20 : * (& Np+Nq) ⊆ * X
              f20 {x} npq with subst (λ k → odef k x) *iso npq
              ... | case1 np = FBase.b⊆X Np np
              ... | case2 nq = FBase.b⊆X Nq nq
              f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
                 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
     --
     -- it contains no empty sets
     -- 
     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
     proper = ?
     --
     -- then we have maximum ultra filter 
     --
     maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
     maxf {X} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
     mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
     mf {X} CSX fp =  MaximumFilter.mf (maxf CSX fp) 
     ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
     ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
     --
     -- so i has a limit as a limit of UIP
     --
     limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
     limit {X} CSX fp with trio< o∅ X
     ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))
     ... | tri≈ ¬a 0=X ¬c = o∅ 
     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
     uf02 : {X v  : Ordinal} → (0<X : o∅ o< X)  → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
        → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
     uf02 {X} {v} 0<X CSX fp nei {x} vx with trio< o∅ X
     ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) nei vx
     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a 0<X )
     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
     --
     -- the limit is an limit of entire elements of X
     --
     uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
     uf01 {X} CSX fp {x} xx with trio< o∅ X
     ... | tri< 0<X ¬b ¬c = ?
     ... | tri≈ ¬a 0=X ¬c = ?
     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )

FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
   →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where
     --
     -- take closure of given filter elements
     --
     CF : HOD
     CF = Replace (filter F) (λ x → Cl TP x  )
     CF⊆CS : CF ⊆ CS TP
     CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 
     --
     -- it is set of closed set and has FIP ( F is proper )
     --
     ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
     ufl01 = ?
     --
     -- so we have a limit
     --
     limit : Ordinal
     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01  
     ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01  
     --
     -- Neigbor of limit ⊆ Filter
     --
     ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅  -- because limit is in CF which is a closure
     ufl03 {f} {v} ff nei fv=0 = ?
     pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
     pp {v} {x} nei vx z pz = ?
     ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 
     ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
     ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
     ... | case2 nfv = ? -- will contradicts ufl03

-- product topology of compact topology is compact

Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
     uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
             → UFLP TP F UF
     uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
     uflQ : (F : Filter {Power Q} {Q} (λ x → x))  (UF : ultra-filter F)
             → UFLP TQ F UF
     uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF
     -- Product of UFL has a limit point
     uflPQ :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
             → UFLP (ProductTopology TP TQ) F UF
     uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
         FP : Filter {Power P} {P} (λ x → x)
         FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
             ty00 {x} ⟪ PPx , ppf ⟫ = PPx
         UFP : ultra-filter FP
         UFP = record { proper = ? ; ultra = ? }
         uflp : UFLP TP FP UFP
         uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP

         FQ : Filter {Power Q} {Q} (λ x → x)
         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
             ty00 {x} ⟪ QPx , ppf ⟫ = QPx
         UFQ : ultra-filter FQ
         UFQ = record { proper = ? ; ultra = ? }
         uflq : UFLP TQ FQ UFQ
         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ

         Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
         Pf = ?
         pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F 
         pq⊆F = ?
         isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F 
         isL {v} npq {x} fx = ? where 
             bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
             bpq = Neighbor.ou npq (Neighbor.ux npq)
             pqb : Subbase (pbase TP TQ) (Base.b bpq )
             pqb = Base.sb bpq 
             pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq )
             pqb⊆opq = Base.b⊆u bpq
             base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆  * (Neighbor.u npq) → * b ⊆ filter F
             base⊆F (gi (case1 px)) b⊆u {z} bz = fz  where
                 -- F contains no od∅, because it projection contains no od∅
                 --    x is an element of BaseP, which is a subset of Neighbor npq
                 --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
                 --    BaseP ∩ F is not empty
                 --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , 
                 il1 : odef (Power P) z ∧ ZProj1 (filter F) z
                 il1 = UFLP.is-limit uflp ? bz 
                 nei1 : HOD
                 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
                 plimit : Ordinal
                 plimit = UFLP.limit uflp 
                 nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
                 nproper = ?
                 b∋z : odef nei1 z
                 b∋z = ?
                 bp : BaseP {P} TP Q z
                 bp = record { p = ? ; op = ? ; prod = ? }
                 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
                 neip = ?
                 il2 : * z ⊆ ZFP (Power P) (Power Q)
                 il2 = ?
                 il3 : filter F ∋ ? 
                 il3 = ?
                 fz : odef (filter F) z
                 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)
             base⊆F (gi (case2 qx)) b⊆u {z} bz = ?
             base⊆F (g∩ b1 b2) b⊆u {z} bz = ?