\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Directed
\import Order.Lattice
\import Order.PartialOrder
\import Paths.Meta
\import Set.Filter
\import Set.Set
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product

\func DirectedCoverSpace (I : DirectedSet) : CoverSpace I
  => RegPrecoverSpace precover
  \where {
    \func precover : PrecoverSpace I \cowith
      | isCauchy C => \Sigma (∃ (U : C) (N : I) (\Pi {n : I} -> N <= n -> U n)) (\Pi (n : I) -> ∃ (V : C) (V n))
      | cauchy-cover => __.
      | cauchy-top => \case I.isInhabitted \with {
        | inP n => (inP (top, idp, n, \lam _ => ()), \lam n => inP (top, idp, ()))
      }
      | cauchy-refine Cc C<D => \case Cc. \with {
          | inP (U,CU,N,g) => (\case C<D CU \with {
            | inP (V,DV,U<=V) => inP (V, DV, N, \lam p => U<=V (g p))
          }, \lam n => \case Cc. n \with {
            | inP (V,CV,Vn) => \case C<D CV \with {
              | inP (W,DW,V<=W) => inP (W, DW, V<=W Vn)
            }
          })
        }
      | cauchy-glue Cc Dc => (\case Cc. \with {
          | inP (U,CU,N,g) => \case (Dc CU). \with {
            | inP (V,DUV,M,h) => \case isDirected N M \with {
              | inP (L,N<=L,M<=L) => inP (U ∧ V, inP (U, V, CU, DUV, idp), L, \lam L<=n => (g $ N<=L <=∘ L<=n, h $ M<=L <=∘ L<=n))
            }
          }
        }, \lam n => \case Cc. n \with {
          | inP (U,CU,Un) => \case (Dc CU). n \with {
            | inP (V,DUV,Vn) => inP (U ∧ V, inP (U, V, CU, DUV, idp), (Un, Vn))
          }
        })

    \lemma makePrecover (N : I) : precover.isCauchy \lam V => (V = \lam n => N <= n) || Given (n : I) (V = single n)
      => (inP (_, byLeft idp, N, \lam p => p), \lam n => inP (single n, byRight (n, idp), idp))
  }

\func EventualityFilter {I : DirectedSet} : CauchyFilter (DirectedCoverSpace I)
  => regPrecoverCauchyFilter (\new ProperFilter {
    | F U => ∃ (N : I) ∀ {n} (N <= n -> U n)
    | filter-mono (inP (N,f)) p => inP (N, \lam q => p $ f q)
    | filter-top => \case I.isInhabitted \with {
      | inP x => inP (x, \lam _ => ())
    }
    | filter-meet (inP (N,f)) (inP (M,g)) => \case isDirected N M \with {
      | inP (L,N<=L,M<=L) => inP (L, \lam p => (f $ N<=L <=∘ p, g $ M<=L <=∘ p))
    }
    | isProper (inP (N,f)) => inP (N, f <=-refl)
  }) $ later \lam (inP (U,CU,N,g), _) => inP (U, CU, inP (N, g))

\func DirectProdCover {I : DirectedSet} {X : CoverSpace} (D : Set (Set (\Sigma I X))) : \Prop
  => \Sigma (X.isCauchy \lam U => ∃ (N : I) (V : D) (\Pi {n : I} {x : X} -> N <= n -> U x -> V (n,x))) (\Pi (n : I) -> X.isCauchy \lam U => ∃ (V : D) ∀ {x : U} (V (n,x)))
  \where {
    \protected \func Space : PrecoverSpace (\Sigma I X) \cowith
      | isCauchy => DirectProdCover
      | cauchy-cover Cc s => \case cauchy-cover (Cc. s.) s. \with {
        | inP (U, inP (V,CV,h), Ux) => inP (V, CV, h Ux)
      }
      | cauchy-top => (top-cauchy \case I.isInhabitted \with {
        | inP N => inP $ later (N, top, idp, \lam _ _ => ())
      }, \lam n => top-cauchy $ inP $ later (top, idp, \lam _ => ()))
      | cauchy-refine Cc C<D => (cauchy-subset Cc. \lam (inP (N,V,CV,p)) => \case C<D CV \with {
        | inP (V',DV',V<=V') => inP $ later (N, V', DV', \lam N<=n Ux => V<=V' $ p N<=n Ux)
      }, \lam n => cauchy-subset (Cc. n) \lam (inP (V,CV,h)) => \case C<D CV \with {
        | inP (V',DV',V<=V') => inP $ later (V', DV', \lam Ux => V<=V' (h Ux))
      })
      | cauchy-glue {C} Cc {D} Dc => (cauchy-glue* Cc. \lam (inP (N,U',CU',Uh)) => cauchy-subset (Dc CU'). \lam (inP (M,V',DU'V',Vh)) => \case isDirected N M \with {
        | inP (L,N<=L,M<=L) => inP $ later (L, U' ∧ V', inP (U',V',CU',DU'V',idp), \lam L<=n s => (Uh (N<=L <=∘ L<=n) s., Vh (M<=L <=∘ L<=n) s.))
      }, \lam n => cauchy-glue* (Cc. n) \lam (inP (U',CU',Uh)) => cauchy-subset ((Dc CU'). n) \lam (inP (V',DU'V',Vh)) => inP $ later (U' ∧ V', inP (U',V',CU',DU'V',idp), \lam s => (Uh s., Vh s.)))
  }

\lemma directedProdCover-char {I : DirectedSet} {X : CoverSpace} {D : Set (Set (\Sigma I X))} : isCauchy {DirectedCoverSpace.precover `ProductPrecoverSpace` X} D <-> DirectProdCover D
  => (ClosurePrecoverSpace.closure-cauchy {_} {DirectProdCover.Space} $ later \case \elim __ \with {
        | inP (_, byLeft idp, (inP (U, inP (V,CV,p), N, g), h)) => (top-cauchy $ inP $ later (N, V, CV, \lam s _ => p $ g s), \lam n => \case h n \with {
          | inP (W, inP (W',CW',WW'), Wn) => top-cauchy $ inP $ later (W', CW', \lam _ => WW' Wn)
        })
        | inP (_, byRight idp, Cc) => (cauchy-subset Cc \lam (inP (V,CV,p)) => \case I.isInhabitted \with {
          | inP N => inP $ later (N, V, CV, \lam _ s => p s)
        }, \lam n => cauchy-subset Cc \lam (inP (V,CV,p)) => inP $ later (V, CV, p __))
      }, \lam Dc => cauchy-glue-refine {DirectedCoverSpace.precover {I} `ProductPrecoverSpace` X} (ProductPrecoverSpace.proj2.func-cover Dc.) \lam {_} (inP (U', inP (N,U,DU,U'U), idp)) =>
          cauchy-glue* {DirectedCoverSpace.precover {I} `ProductPrecoverSpace` X} (ProductPrecoverSpace.proj1.func-cover (DirectedCoverSpace.makePrecover N)) \lam {V} => \case \elim V, \elim __ \with {
            | _, inP (_, byLeft idp, idp) => top-cauchy {DirectedCoverSpace.precover `ProductPrecoverSpace` X} $ inP $ later (U, DU, \lam s => U'U s.. s.)
            | _, inP (_, byRight (n,idp), idp) => cauchy-subset {DirectedCoverSpace.precover {I} `ProductPrecoverSpace` X} (ProductPrecoverSpace.proj2.func-cover (Dc. n))
              \lam {_} (inP (W', inP (Vn,DVn,h), idp)) => inP $ later (Vn, DVn, \lam {x} (_,s) => rewrite s. in h s.)
          })