Maria Emilia Maietti ; Pietro Sabelli - A topological counterpart of well-founded trees in dependent type theory

entics:11755 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX - https://doi.org/10.46298/entics.11755
A topological counterpart of well-founded trees in dependent type theoryArticle

Authors: Maria Emilia Maietti ; Pietro Sabelli

    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.


    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: September 4, 2023
    Submitted on: August 22, 2023
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    Consultation statistics

    This page has been seen 104 times.
    This article's PDF has been downloaded 72 times.