open import Level
open import Ordinals
module Topology {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.PropositionalEquality
import BAlgbra 
open BAlgbra 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


record Topology  ( L : HOD ) : Set (suc n) where
   field
       OS    : HOD
       OS⊆PL :  OS ⊆ Power L 
       o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
       o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)
-- closed Set
   CS : HOD
   CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
       tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
       tp02 {y} nop = ?
   os⊆L :  {x : HOD} → OS ∋ x → x ⊆ L 
   os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy  )
       -- ∈∅< ( proj1 nop )

open Topology

-- Base
-- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that 
-- W ⊆ U ∩ V and x ∈ W .

data Subbase (P : HOD) : Ordinal → Set n where
   gi : {x : Ordinal } → odef P x → Subbase P x
   g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))

Subbases : (P : HOD) → HOD
Subbases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }

record Base (P : HOD) (x : Ordinal) : Set n where
   field
       b   : Ordinal
       pb  : odef (Power (Subbases P) ) b
       bx : odef (* b) x

GeneratedTop : (P : HOD) → HOD
GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }

record IsBase (L P : HOD) : Set (suc n) where
   field
       p : {x : HOD} → L ∋ x → HOD
       in-P : {x : HOD} → (lx : L ∋ x ) → P ∋ p lx
       b∩   : {x y : HOD} → (bx : P ∋ x ) (by : P ∋ y ) → HOD
       b∩⊂  : {x y z : HOD} → {bx : P ∋ x } {by : P ∋ y } → ( x ∩ y ) ∋  z → ( b∩ bx by ∋ x ) ∧ ( b∩ bx by  ⊆ ( x ∩ y )   )

GeneratedIsTopogy : (P L : HOD) → IsBase L P  → Topology L
GeneratedIsTopogy = ?

-- covers

record _covers_ ( P q : HOD  ) : Set (suc n) where
   field
       cover   : {x : HOD} → q ∋ x → HOD
       P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
       isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x

-- Finite Intersection Property

data Finite-∩ (S : HOD) : HOD → Set (suc n) where
   fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
   fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)

record FIP {L : HOD} (top : Topology L) : Set (suc n) where
   field
       fipS⊆PL :  L ⊆ CS top
       fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )

-- Compact

data Finite-∪ (S : HOD) : HOD → Set (suc n) where
   fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
   fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)

record Compact  {L : HOD} (top : Topology L)  : Set (suc n) where
   field
       finCover  : {X : HOD} → X ⊆ OS top → X covers L → HOD
       isCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp  )

-- FIP is Compact

FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top 
FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }

Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top 
Compact→FIP = {!!}

-- Product Topology

open ZFProduct 

record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
   field
       p q : Ordinal
       op : odef (OS TP) p
       prod : x ≡ & (ZFP (* p) Q )

record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
   field
       p q  : Ordinal
       oq : odef (OS TQ) q
       prod : x ≡ & (ZFP P (* q ))

-- box : HOD
-- box = ZFP (OS TP) (OS TQ) 

base : {P Q : HOD} → Topology P → Topology Q → HOD
base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }

POS : {P Q : HOD} → Topology P → Topology Q → HOD
POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)

PU : {A B : HOD} → Power A ∋ B → Power A ∋ Union B
PU = ?

_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
_Top⊗_ {P} {Q} TP TQ = record {
       OS    = POS TP TQ
    ;  OS⊆PL = tp10
    ;  o∪ = tp13
    ;  o∩ = tp14
  } where
        --  B : (OS P ∋ x →  proj⁻¹ x ) ∨ (OS Q ∋ y  →  proj⁻¹ y )
        --  U ⊂ ZFP P Q  ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧  b ⊂ U )
        tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x
        tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12  where
             tp12 : ZFProduct P Q x
             tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso)  zx
             ... | ab-pair pa qb = ZFP→ 
                  (os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op ) (subst (λ k → odef (* p) k) (sym &iso) pa) ) 
                  (subst (λ k → odef Q k ) (sym &iso) qb )
        tp11 {x} {z} (gi (case2 record { p = p ; q = q ; oq = oq ; prod = z=zfp })) zx = tp12  where
             tp12 : ZFProduct P Q x
             tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso)  zx
             ... | ab-pair pa qb = ZFP→  
                  (subst (λ k → odef P k ) (sym &iso) pa ) 
                  ((os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq )) (subst (λ k → odef (* q) k) (sym &iso) qb)  )
        tp11 {x} (g∩ {a} {b} sb sb₁) zx = tp11 sb (proj1 (subst (λ k → odef k x) *iso zx )) 
        tp10 : POS TP TQ ⊆ Power (ZFP P Q)
        tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz
        tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
        tp13 {U} U⊆O  = tp20 U U⊆O where
             ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x
             ind {x} prev x⊆O = record { b = & ub ; pb = ? ; bx = ? } where
                ub : HOD
                ub = Union ( Replace' x ( λ z xz → * (Base.b (x⊆O xz) )  ) )
                tp14 : ub ∋ Union x
                tp14 = ?
             tp20 : (U : HOD ) →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U 
             tp20 U U⊆O = ε-induction0 { λ U →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U } ind U U⊆O
        tp14 :  {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q)
        tp14 {p} {q} op oq  = record { b = & tp15 ; pb = ? ; bx = ? } where
             tp15 : HOD
             tp15 = ?

-- existence of Ultra Filter 

open Filter 

-- Ultra Filter has limit point

record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
   field
       limit : Ordinal
       P∋limit : odef P limit
       is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F

-- FIP is UFL

FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP 
   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf 
FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }

UFLP→FIP : {P : HOD} (TP : Topology P) → 
   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP 
UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? }

-- Product of UFL has limit point (Tychonoff)

Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (TP Top⊗ TQ)
Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
    uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
            (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
    uflp {L} LPQ F uf = record { limit = & < * ( UFLP.limit uflpp) , ? >  ; P∋limit = ? ; is-limit = ? } where
         LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD  
         LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
         LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P
         LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) 
           (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) )  xw) where
             tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P
             tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1)  ) 
                  (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where
                    tp03 : odef (* z) z1 →  odef (* (& (* z))) (& (* z1)) 
                    tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
         FP : Filter (LPP L LPQ)
         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where
             tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ
             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } 
         uFP : ultra-filter FP
         uFP = record { proper = ? ; ultra = ? }
         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP
         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP 
         LQ : HOD  
         LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
         LQQ : LQ ⊆ Power Q
         LQQ = ?