A topological reading of inductive and coinductive definitions in Dependent Type Theory
Pietro Sabelli
TL;DR
The paper addresses how coinductive predicates in dependent type theory admit a topological reading via coinductively generated positivity relations from Formal Topology. It develops this correspondence within the Minimalist Foundation and is complemented by a parallel treatment in Martin-Löf's type theory, using $M$-types and endofunctors to relate to formal-topology notions. The main contributions are (i) establishing equivalences between coinductive predicates and topological positivity relations in MF, (ii) extending the correspondence to Martin-Löf type theory with proof-relevant (co)induction, and (iii) detailing compatibility results across foundational frameworks, aided by Agda formalizations. The work advances predicative, constructive representations of closed subsets and non-wellfounded structures, with potential implications for predicative formal topologies and their realizability interpretations.
Abstract
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öf's type theory are formalised in the Agda proof assistant.