A topological counterpart of well-founded trees in dependent type theory
Maria Emilia Maietti, Pietro Sabelli
TL;DR
This work establishes a topological counterpart to well-founded trees within constructive dependent type theory by linking W-types, dependent W-types, well-founded predicates, and inductively generated basic covers. It shows that, under mild extensional assumptions, these constructors are propositionally mutually encodable in Homotopy Type Theory and definitionally encodable in Agda, with analogous results in the Minimalist Foundation through well-founded predicates. The authors introduce a formal bridge via well-founded predicates to separate propositions from sets, and provide detailed encodings and mutual encodings across MLTT0, MF, and emTT, all machine-checked in Agda. The results unify inductive topology and dependent type theory, offering a predicative, constructive framework for formal topology and enriching the understanding of inductive constructions in two-level foundations. The work also outlines future directions toward coinductive extensions and positivity relations in topological settings.
Abstract
Within dependent type theory, we provide a topological counterpart of well-founded trees (for short, W-types) by using a proof-relevant version of the notion of inductively generated suplattices introduced in the context of formal topology under the name of inductively generated basic covers. In more detail, we show, firstly, that in Homotopy Type Theory, W-types and proof relevant inductively generated basic covers are propositionally mutually encodable. Secondly, we prove they are definitionally mutually encodable in the Agda implementation of intensional Martin-Loef's type theory. Finally, we reframe the equivalence in the Minimalist Foundation framework by introducing well-founded predicates as the logical counterpart for predicates of dependent W-types. All the results have been checked in the Agda proof-assistant.