{
  "id": "0811.2774",
  "version": "v4",
  "published": "2008-11-17T19:24:28.000Z",
  "updated": "2024-04-03T08:30:16.000Z",
  "title": "A minimalist two-level foundation for constructive mathematics",
  "authors": [
    "Maria Emilia Maietti"
  ],
  "comment": "46 pages, revised version (I corrected typos and omissions in the definition of canonical isomorphisms)",
  "journal": "Annals of Pure and Applied Logic, Volume 160, Issue 3, September 2009, Pages 319-354",
  "doi": "10.1016/j.apal.2009.01.006",
  "categories": [
    "math.LO"
  ],
  "abstract": "We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends the set-theoretic version introduced in the mentioned paper with collections. The other level is given by an extensional set theory which is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the \"proofs-as-programs\" paradigm and acts as a programming language.",
  "revisions": [
    {
      "version": "v3",
      "updated": "2011-10-17T17:37:14.000Z",
      "comment": "46 pages, revised version (I corrected typos)",
      "journal": null,
      "doi": null
    },
    {
      "version": "v4",
      "updated": "2024-04-03T08:30:16.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03G30",
      "03B15",
      "18C50",
      "03B20",
      "03F55"
    ],
    "keywords": [
      "minimalist two-level foundation",
      "constructive mathematics",
      "two-level theory",
      "intensional type theory",
      "minimal type theory"
    ],
    "tags": [
      "journal article"
    ],
    "publication": {
      "publisher": "Elsevier"
    },
    "note": {
      "typesetting": "TeX",
      "pages": 46,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2008arXiv0811.2774E"
    }
  }
}