Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The de
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Fondements univalents (fr)
- Univalent foundations (en)
|
| rdfs:comment
| - Parmi les fondements des mathématiques, les fondements univalents sont une approche des fondements des mathématiques constructives basée sur l'idée que les mathématiques étudient des structures de "types univalents" qui correspondent, en projection sur la théorie des ensembles, aux types d'homotopie. Les fondements univalents sont inspirés à la fois par les idées Platoniciennes de Hermann Grassmann et Georg Cantor et par la théorie des "catégories" d'Alexander Grothendieck. Ils s'écartent de la logique des prédicats comme système sous-jacent de la déduction formelle, en la remplaçant par une version de la théorie des types de Martin-Löf. Le développement des fondements univalents est étroitement lié au développement de la théorie des types homotopiques. (fr)
- Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The de (en)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - Parmi les fondements des mathématiques, les fondements univalents sont une approche des fondements des mathématiques constructives basée sur l'idée que les mathématiques étudient des structures de "types univalents" qui correspondent, en projection sur la théorie des ensembles, aux types d'homotopie. Les fondements univalents sont inspirés à la fois par les idées Platoniciennes de Hermann Grassmann et Georg Cantor et par la théorie des "catégories" d'Alexander Grothendieck. Ils s'écartent de la logique des prédicats comme système sous-jacent de la déduction formelle, en la remplaçant par une version de la théorie des types de Martin-Löf. Le développement des fondements univalents est étroitement lié au développement de la théorie des types homotopiques. Les fondements univalents sont compatibles avec le structuralisme dans la mesure où une notion de structure mathématique appropriée (c.à.d. catégorique) est adoptée. (fr)
- Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory. Univalent foundations are compatible with structuralism, if an appropriate (i.e., categorical) notion of mathematical structure is adopted. (en)
|
| gold:hypernym
| |
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage disambiguates
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)