{
  "id": "1809.02375",
  "version": "v1",
  "published": "2018-09-07T09:45:08.000Z",
  "updated": "2018-09-07T09:45:08.000Z",
  "title": "W-types in setoids",
  "authors": [
    "Jacopo Emmenegger"
  ],
  "comment": "18 pages; formalised in Coq",
  "categories": [
    "math.LO"
  ],
  "abstract": "W-types and their categorical analogue, initial algebras for polynomial endofunctors, are an important tool in predicative systems to replace transfinite recursion on well-orderings. Current arguments to obtain W-types in quotient completions rely on assumptions, like Uniqueness of Identity Proofs, or on constructions that involve recursion into a universe, that limit their applicability to a specific setting. We present an argument, verified in Coq, that instead uses dependent W-types in the underlying type theory to construct W-types in the setoid model. The immediate advantage is to have a proof more type-theoretic in flavour, which directly uses recursion on the underlying W-type to prove initiality. Furthermore, taking place in intensional type theory and not requiring any recursion into a universe, it may be generalised to various categorical quotient completions, with the aim of finding a uniform construction of extensional W-types.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2018-09-07T09:45:08.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B15",
      "03F55",
      "18D35",
      "18B05"
    ],
    "keywords": [
      "quotient completions",
      "replace transfinite recursion",
      "intensional type theory",
      "dependent w-types",
      "current arguments"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 18,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}