[Agda] Libraries for (finite) topological spaces?

[Eduardo Ochs]

Hi list,

I am working on something - Grothendieck Topologies on topologies on
finite sets - that I would like to formalize in Agda. I tried to find
Agda's libraries for topological spaces to use them as a starting
point, but both googling and grepping returned practically nothing...
Any recommendations? I mean, besides "try to adapt the code for
Heyting Algebras"?

  Thanks in advance!
    Eduardo Ochs
    http://angg.twu.net/math-b.html