W-types in setoids
From MaRDI portal
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.
Recommendations
- Setoids in type theory
- W-types in homotopy type theory
- From type theory to setoids and back
- Constructing categories and setoids of setoids in type theory
- Multisets in type theory
- Sets in homotopy type theory
- Setoid type theory -- a syntactic translation
- Type inference for set theory
- scientific article; zbMATH DE number 1420782
- scientific article; zbMATH DE number 1088050
Cites work
- A minimalist two-level foundation for constructive mathematics
- A set constructor for inductive sets in Martin-Löf's type theory
- Constructing categories and setoids of setoids in type theory
- Exact completion and constructive theories of sets
- Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
- Homotopy type theory. Univalent foundations of mathematics
- Homotopy-initial algebras in type theory
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 4012604 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- Inductive types and exact completion
- Polynomial functors and polynomial monads
- Proof-relevance of families of setoids and identity in type theory
- Quotient completion for the foundation of constructive mathematics
- Relating quotient completions via categorical logic
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Setoids in type theory
- Sets in homotopy type theory
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- Types for Proofs and Programs
- Wellfounded trees in categories
Cited in
(7)
This page was built for publication: W-types in setoids
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5155691)
