\import Category
\import Category.Meta
\import Logic.Meta
\import Paths.Meta
\import Set
\import Set.Category

\class TopSpace \extends BaseSet
  | topology : (E -> \Prop) -> \Prop
  | top-top : topology (\lam _ => \Sigma)
  | top-meet {P Q : E -> \Prop} : topology P -> topology Q -> topology (\lam x => \Sigma (P x) (Q x))
  | top-Join (S : (E -> \Prop) -> \Prop) : (\Pi (P : E -> \Prop) -> S P -> topology P) -> topology (\lam x => ∃ (P : E -> \Prop) (S P) (P x))

\class TopHom \extends SetHom {
  \override Dom : TopSpace
  \override Cod : TopSpace
  | func-topology (U : Cod -> \Prop) : topology U -> topology (\lam x => U (func x))
}

\instance TopCat : Cat TopSpace
  | Hom => TopHom
  | id X => \new TopHom {
    | func x => x
    | func-topology U t => t
  }
  | o g f => \new TopHom {
    | func x => g (f x)
    | func-topology U t => func-topology {f} (\lam y => U (g y)) (func-topology {g} U t)
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {S1} {S2} h1 h2 => exts (\lam U => ext (func-topology {h2} U, func-topology {h1} U)))