A topological counterpart of well-founded trees in dependent type theory

TL;DR

This paper establishes a topological perspective on well-founded trees in dependent type theory, demonstrating their equivalence with inductively generated basic covers across multiple type-theoretic frameworks, verified in Agda.

Contribution

It introduces a topological counterpart to W-types using inductively generated basic covers and proves their equivalence in Homotopy Type Theory, Agda, and the Minimalist Foundation.

Findings

W-types and inductively generated basic covers are mutually encodable in Homotopy Type Theory.

They are also mutually encodable in Agda's intensional Martin-Löf type theory.

The equivalence is reframed in the Minimalist Foundation with well-founded predicates.

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.