\import Function.Meta
\import Logic
\import Logic.Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths.Meta
\import Set.Subset

\record Filter (A : TopMeetSemilattice) (\coerce F : A -> \Prop)
  | filter-mono {a b : A} : F a -> a <= b -> F b
  | filter-top : F top
  | filter-meet {a b : A} : F a -> F b -> F (a ∧ b)
  \where {
    \func principal {A : TopMeetSemilattice} (a : A) : Filter A \cowith
      | F => a <=
      | filter-mono => <=∘
      | filter-top => top-univ
      | filter-meet => meet-univ
  }

\record CompleteFilter \extends Filter {
  \override A : CompleteLattice
  | filter-Join {J : \Set} {f : J -> A} : F (Join f) -> ∃ (j : J) (F (f j))

  \lemma isProper (p : F CompleteLattice.bottom) : Empty
    => \case filter-Join {_} {Empty} {absurd} (filter-mono p CompleteLattice.bottom-univ) \with {
      | inP (e,_) => e
    }
}

\record SetFilter (X : \Set) \extends Filter
  | A => SetLattice X

\func SetFilter-map {X Y : \Set} (f : X -> Y) (F : SetFilter X) : SetFilter Y \cowith
  | F V => F (f ^-1 V)
  | filter-mono d p => filter-mono d (p __)
  | filter-top => filter-top
  | filter-meet => filter-meet

\record WeaklyProperFilter \extends SetFilter
  | isWeaklyProper : Not (F bottom)

\record ProperFilter \extends WeaklyProperFilter
  | isProper {U : Set X} : F U -> ∃ U
  | isWeaklyProper Fb => \case isProper Fb \with {
    | inP (x, inP ((),_))
  }

\func pointFilter {X : \Set} (x : X) : ProperFilter X \cowith
  | F U => U x
  | filter-mono d p => p d
  | filter-top => ()
  | filter-meet p q => (p,q)
  | isProper Ux => inP (x,Ux)

\func WeaklyProperFilter-map {X Y : \Set} (f : X -> Y) (F : WeaklyProperFilter X) : WeaklyProperFilter Y \cowith
  | SetFilter => SetFilter-map f F
  | isWeaklyProper d => F.isWeaklyProper $ F.filter-mono d \lam (inP ((),_))

\func ProperFilter-map {X Y : \Set} (f : X -> Y) (F : ProperFilter X) : ProperFilter Y \cowith
  | SetFilter => SetFilter-map f F
  | isProper d => TruncP.map (isProper d) \lam s => (f s., s.)

\instance WeaklyProperFilterSemilattice (X : \Set) : MeetSemilattice (WeaklyProperFilter X)
  | <= F G => F ⊆ G
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => exts \lam U => ext (f,g)
  | meet F G => \new WeaklyProperFilter {
    | F U => \Sigma (F U) (G U)
    | filter-mono s p => (filter-mono s. p, filter-mono s. p)
    | filter-top => (filter-top, filter-top)
    | filter-meet s t => (filter-meet s. t., filter-meet s. t.)
    | isWeaklyProper s => isWeaklyProper s.
  }
  | meet-left s => s.
  | meet-right s => s.
  | meet-univ f g c => (f c, g c)

\instance ProperFilterSemilattice (X : \Set) : MeetSemilattice (ProperFilter X)
  | <= F G => F ⊆ G
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => exts \lam U => ext (f,g)
  | meet F G => \new ProperFilter {
    | F U => \Sigma (F U) (G U)
    | filter-mono s p => (filter-mono s. p, filter-mono s. p)
    | filter-top => (filter-top, filter-top)
    | filter-meet s t => (filter-meet s. t., filter-meet s. t.)
    | isProper s => isProper s.
  }
  | meet-left s => s.
  | meet-right s => s.
  | meet-univ f g c => (f c, g c)