A meaning explanation for HoTT.
In the Univalent Foundations of mathematics spatial notions like "point" and "path" are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Ho...
| Publicado en: | Synthese Vol. 197; no. 2; pp. 651 - 681 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Springer Nature
Feb2020
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=142062010&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 142062010 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00397857 4LI jtl: Synthese issn: 00397857 maglogo: N pubinfo: dt: Feb2020 vid: 197 iid: 2 pid: 237 pub: Springer Nature artinfo: ui: 142062010 10.1007/s11229-018-02052-1 ppf: 651 ppct: 30 formats: fmt: – @attributes: type: T – @attributes: type: P size: 758KB tig: atl: A meaning explanation for HoTT. aug: au: Tsementzis, Dimitris affil: 11201, Brooklyn, NY, USA su: Homotopy theory Explanation Set theory Mathematics sug: subj: Homotopy theory Explanation Set theory Mathematics keyword: Homotopy type theory Meaning explanation Univalent foundations ab: In the Univalent Foundations of mathematics spatial notions like "point" and "path" are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory (as a formalism for the Univalent Foundations) can be justified intuitively as a theory of shapes in the same way that ZFC (as a formalism for set-theoretic foundations) can be justified intuitively as a theory of collections. I first clarify what such an "intuitive justification" should be by distinguishing between formal and pre-formal "meaning explanations" in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like "shape", "path" etc. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y custom: Synthese is a copyright of Springer, 2020. All Rights Reserved. item: Synthese holder: Springer Nature dt: @attributes: year: 2020 holdings: @attributes: islocal: N |
|---|