TL;DR
This paper constructs W-types within the setoid model of extensional Martin-Löf type theory using dependent W-types, demonstrating initial algebra existence for polynomial endofunctors in the setoid category.
Contribution
It introduces a novel method for constructing W-types in the setoid model via dependent W-types, avoiding universe elimination, and formalizes the results in Coq.
Findings
Initial algebras for polynomial endofunctors exist in the setoid category.
Setoids of algebra morphisms are characterized as dependent W-types.
Formal verification of results in Coq is provided.
Abstract
We present a construction of W-types in the setoid model of extensional Martin-L\"of 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
