  In the context of dependent type theory, we show that coinductive predicates
have an equivalent topological counterpart in terms of coinductively generated
positivity relations, introduced by G. Sambin to represent closed subsets in
point-free topology. Our work is complementary to a previous one with M.E.
Maietti, where we showed that, in dependent type theory, the well-known concept
of wellfounded trees has a topological equivalent counterpart in terms of
proof-relevant inductively generated formal covers used to provide a
predicative and constructive representation of complete suplattices. All proofs
in Martin-L\"of's type theory are formalised in the Agda proof assistant.
