Univalent foundations (original) (raw)
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.
| Property | Value |
|---|---|
| dbo: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) |
| dbo:wikiPageExternalLink | https://github.com/HoTT/HoTT https://github.com/UniMath/UniMath/tree/master/UniMath/Foundations https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html |
| dbo:wikiPageID | 44554214 (xsd:integer) |
| dbo:wikiPageLength | 14282 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1075466442 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Predicate_logic dbr:Coq_(proof_assistant) dbr:Homotopy_type_theory dbr:Univalence_axiom dbr:Vladimir_Voevodsky dbr:Georg_Cantor dbr:Structuralism_(philosophy_of_mathematics) dbr:Agda_(programming_language) dbr:Alexander_Grothendieck dbr:Partially_ordered_set dbr:Diagram_(category_theory) dbr:Foundations_of_mathematics dbr:Hermann_Grassmann dbr:Thierry_Coquand dbr:Higher_category_theory dbr:Homotopy dbr:Axiom_of_choice dbc:Foundations_of_mathematics dbr:Philosophy_of_mathematics dbr:Michael_Shulman_(mathematician) dbr:Category_theory dbr:Calculus_of_Inductive_Constructions dbr:Séminaire_Nicolas_Bourbaki dbr:Michael_Makkai dbr:Simplicial_set dbr:Martin-Löf_type_theory dbr:Infinity_groupoid dbr:Constructive_mathematics dbr:Excluded_middle dbr:Marc_Bezem dbr:Simon_Huber dbr:UniMath |
| dbp:wikiPageUsesTemplate | dbt:Citation dbt:Efn dbt:Notelist dbt:Reflist dbt:Rp dbt:Wiktionary-inline dbt:Foundations-footer |
| dct:subject | dbc:Foundations_of_mathematics |
| gold:hypernym | dbr:Approach |
| rdf:type | dbo:ProgrammingLanguage |
| 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) |
| rdfs:label | Fondements univalents (fr) Univalent foundations (en) |
| owl:sameAs | freebase:Univalent foundations yago-res:Univalent foundations wikidata:Univalent foundations dbpedia-fr:Univalent foundations https://global.dbpedia.org/id/2NsTh |
| prov:wasDerivedFrom | wikipedia-en:Univalent_foundations?oldid=1075466442&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Univalent_foundations |
| is dbo:wikiPageDisambiguates of | dbr:Univalent |
| is dbo:wikiPageWikiLink of | dbr:Applied_category_theory dbr:Homotopy_type_theory dbr:Vladimir_Voevodsky dbr:Equality_(mathematics) dbr:Structuralism_(philosophy_of_mathematics) dbr:QED_manifesto dbr:Michael_Shulman_(mathematician) dbr:Set_theory dbr:Univalent dbr:Thorsten_Altenkirch |
| is foaf:primaryTopic of | wikipedia-en:Univalent_foundations |