\import Data.Array
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Topology.Locale
\open Bounded(top,top-univ)

\func Set (X : \hType) => X -> \Prop
  \where {
    \func Union {X : \hType} (S : Set X -> \hType) : Set X
      => \lam a => ∃ (U : S) (U a)

    \lemma Union-cond {X : \hType} {S : Set X -> \hType} {U : Set X} (SU : S U) : U ⊆ Union S
      => \lam Ux => inP (U,SU,Ux)

    \func Total {X : \Type} (U : Set X) => \Sigma (x : X) (U x)

    \func restrict {X : \Type} {U : Set X} (V : Set X) : Set (Total U)
      => \lam s => V s.

    \func Prod {X Y : \hType} (U : Set X) (V : Set Y) : Set (\Sigma X Y)
      => \lam s => \Sigma (U s.) (V s.)

    \func CoverInter {X : \hType} (C : Set (Set X)) (D : Set (Set X)) : Set (Set X)
      => \lam W => ∃ (U : C) (V : D) (W = U ∧ {SetLattice X} V)

    \func CoverInterBig {X : \hType} (Cs : Array (Set (Set X))) : Set (Set X)
      => Big CoverInter (single (top {SetLattice X})) Cs
  }

\func single {X : \Set} (a : X) : Set X
  => a =

\lemma single_<= {X : \Set} {a : X} {U : Set X} (Ua : U a) : single a ⊆ U
  => \lam p => rewriteI p Ua

\func \infix  ^-1 {X Y : \hType} (f : X -> Y) (S : Set Y) : Set X
  => \lam a => S (f a)

\type Subset \alias \infix  ⊆ {X : \hType} (U V : Set X) => \Pi {x : X} -> U x -> V x

\func Compl {X : \hType} (U : Set X) : Set X
  => \lam x => Not (U x)

\instance SetLattice (A : \hType) : Locale (Set A)
  | <= => ⊆
  | <=-refl p => p
  | <=-transitive p q u => q (p u)
  | <=-antisymmetric p q => ext \lam x => ext (p,q)
  | meet U V a => \Sigma (U a) (V a)
  | meet-left => __.
  | meet-right => __.
  | meet-univ p q c => (p c, q c)
  | top _ => \Sigma
  | top-univ _ => ()
  | Join {J} f a => ∃ (j : J) (f j a)
  | Join-cond j c => inP (j,c)
  | Join-univ d (inP (j,c)) => d j c
  | Join-ldistr>= (d, inP (j,c)) => inP (j,(d,c))

\func Refines {X : \hType} (C D : Set (Set X)) : \Prop
  => ∀ {U : C} ∃ (V : D) (U ⊆ V)

\lemma Refines-cover {X : \hType} {C D : Set (Set X)} (r : Refines C D) {x : X} (p : ∃ (U : C) (U x)) : ∃ (V : D) (V x) \elim p
  | inP (U,CU,Ux) => \case r CU \with {
    | inP (V,DV,U<=V) => inP (V, DV, U<=V Ux)
  }

\lemma Refines-single_top {X : \hType} {C : Set (Set X)} : Refines C (single top)
  => \lam _ => inP (top, idp, top-univ)

\lemma Refines-refl {X : \hType} {C : Set (Set X)} : Refines C C
  => \lam CU => inP (_, CU, <=-refl)

\lemma Refines-trans {X : \hType} {C D E : Set (Set X)} (r1 : Refines C D) (r2 : Refines D E) : Refines C E
  => \lam CU => \case r1 CU \with {
    | inP (V,DV,U<=V) => \case r2 DV \with {
      | inP (W,EW,V<=W) => inP (W, EW, U<=V <=∘ V<=W)
    }
  }

\lemma Refines-inter-left {X : \hType} {C D : Set (Set X)} : Refines (Set.CoverInter C D) C
  => \lam {_} (inP (U,CU,_,_,idp)) => inP (U, CU, meet-left)

\lemma Refines-inter-right {X : \hType} {C D : Set (Set X)} : Refines (Set.CoverInter C D) D
  => \lam {_} (inP (_,_,V,DV,idp)) => inP (V, DV, meet-right)

\lemma Refines-inter-big {X : \hType} (Cs : Array (Set (Set X))) (j : Fin Cs.len) : Refines (Set.CoverInterBig Cs) (Cs j) \elim Cs, j
  | C :: Cs,  => Refines-inter-left
  | C :: Cs, suc j => Refines-trans Refines-inter-right (Refines-inter-big Cs  j)

\lemma Refines-inter {X : \hType} {C D C' D' : Set (Set X)} (r : Refines C D) (r' : Refines C' D') : Refines (Set.CoverInter C C') (Set.CoverInter D D')
  => \lam {W} (inP (U,CU,U',C'U',W=UU')) => \case r CU, r' C'U' \with {
    | inP (V,DV,U<=V), inP (V',D'V',U'<=V') => inP (V ∧ V', inP (V, DV, V', D'V', idp), rewrite W=UU' $ MeetSemilattice.meet-monotone U<=V U'<=V')
  }

\lemma CoverInterBig-char {X : \hType} {Cs : Array (Set (Set X))} : Set.CoverInterBig Cs = \lam W => ∃ (Us : Array (Set X) Cs.len) (\Pi (j : Fin Cs.len) -> Cs j (Us j)) (W = Big {Set X} (∧) top Us) \elim Cs
  | nil => exts \lam W => ext (\lam p => inP (nil, \case __ \with {}, inv p), \lam (inP t) => inv t.)
  | C :: Cs => pmap (Set.CoverInter C) CoverInterBig-char *> exts \lam W => ext (
      \lam (inP (U, CU, V, inP (Us,CsUs,q), p)) => inP (U :: Us, \case \elim __ \with {
        |  => CU
        | suc j => CsUs j
      }, p *> pmap (U ∧) q),
      \lam (inP (Us,CsUs,p)) => inP (Us , CsUs , _, inP (\lam j => Us (suc j), \lam j => CsUs (suc j), idp), p))

\func extend {X : \Type} {U : Set X} (V : Set (Set.Total U)) : Set X
  => \lam x => \Sigma (Ux : U x) (V (x,Ux))

\lemma extend-sub {X : \Type} {U : Set X} {V : Set (Set.Total U)} : extend V ⊆ U
  => __.

\lemma extend-mono {X : \Type} {U : Set X} {V W : Set (Set.Total U)} (p : V ⊆ W) : extend V ⊆ extend W
  => \lam {x} (Ux,Vx) => (Ux, p Vx)

\lemma extend_meet {X : \Type} {U : Set X} {V W : Set (Set.Total U)} : extend (V ∧ W) = extend V ∧ extend W
  => <=-antisymmetric (\lam e => ((e., e..), (e., e..))) (\lam e => (e.., (e.., transport W (ext idp) e..)))

\lemma restrict_extend {X : \Type} {U : Set X} {V : Set (Set.Total U)} : Set.restrict (extend V) = V
  => <=-antisymmetric (\lam r => transport V (ext idp) r.) (\lam {x} Vx => (x.,Vx))

\lemma extend_restrict {X : \Type} {U : Set X} {V : Set X} : extend (Set.restrict {X} {U} V) ⊆ V
  => __.

\lemma ^-1_<= {A B : \hType} (f : A -> B) {U V : Set B} (p : U ⊆ V) : f ^-1 U ⊆ f ^-1 V
  => p __

\func ^-1_FrameHom {A B : \hType} (f : A -> B) : FrameHom (SetLattice B) (SetLattice A) \cowith
  | func => ^-1 f
  | func-<= p {_} => p
  | func-top>= {_} _ => ()
  | func-meet>= c => c
  | func-Join>= c => c