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

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 ZProduct O
-- open import maximum-filter O

open Filter

Filter-Proj1 : {P Q : HOD } → 
     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
      →    Filter {Power P} {P} (λ x → x) 
Filter-Proj1 = ?

Filter-Proj1-UF : {P Q : HOD } → 
     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
      →   (FP :  Filter {Power P} {P} (λ x → x) ) →   ultra-filter FP
Filter-Proj1-UF = ?

filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
    → odef x z → odef (ZFP P Q) z
filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz )

rcf :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx))
rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly }

Filter-sym : {P Q a : HOD } → ZFP P Q ∋ a → 
     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
     → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x)
Filter-sym {P} {Q} {z} pqz F = 
    record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = ? }  where
    fqp : HOD
    fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf  F)
    fqp<P : fqp ⊆ Power (ZFP Q P)
    fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = 
         ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) 
            (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) 
    f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q
    f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 
      ; x=ψz = ? }  where
         q⊆ZQP : q ⊆ ZFP Q P
         q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) 
         p⊆ZQP : p ⊆ ZFP Q P
         p⊆ZQP {z} px = q⊆ZQP (p⊆q px)
         fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp))))
         fig06 = Replaced1.x=ψz fqp
         fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
         fig03 with Replaced1.az fqp 
         ... | fz = subst (λ k → odef (filter F) k ) ?  fz where
             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ px → QPq x (subst (λ k → def (HOD.od k) x) (sym *iso) (p⊆q px))))
             fig07 = ?
         fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP
         fig01 x xz  = ? -- 
         fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
         fis00 = filter1 F 
         fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP
         fis04 = ? 
         fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP)))
             (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04))))
         fis05 = ?



Filter-sym-UF : {P Q : HOD } → 
     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
     → (FQP : Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) )
     → ultra-filter FQP
Filter-sym-UF = ?

Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → 
     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
      →    Filter {Power Q} {Q} (λ x → x) 
Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} (Filter-sym pqa F )