Jacopo Emmenegger - W-types in setoids

lmcs:5764 - Logical Methods in Computer Science, September 24, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:28)2021
W-types in setoids

Authors: Jacopo Emmenegger ORCID-iD

    We present a construction of W-types in the setoid model of extensional Martin-Löf type theory using dependent W-types in the underlying intensional theory. More precisely, we prove that the internal category of setoids has initial algebras for polynomial endofunctors. In particular, we characterise the setoid of algebra morphisms from the initial algebra to a given algebra as a setoid on a dependent W-type. We conclude by discussing the case of free setoids. We work in a fully intensional theory and, in fact, we assume identity types only when discussing free setoids. By using dependent W-types we can also avoid elimination into a type universe. The results have been verified in Coq and a formalisation is available on the author's GitHub page.

    Volume: Volume 17, Issue 3
    Published on: September 24, 2021
    Accepted on: August 2, 2021
    Submitted on: September 16, 2019
    Keywords: Mathematics - Logic,03B15, 03F55, 18D35, 18B05,F.4.1,D.1.1

    Consultation statistics

    This page has been seen 569 times.
    This article's PDF has been downloaded 186 times.