From 46426db83051388ff57475391a34b31ea136ad94 Mon Sep 17 00:00:00 2001 From: Sebastian Englbrecht Date: Tue, 10 Sep 2024 20:04:36 +0200 Subject: [PATCH 1/4] add blog draft about infinity cosmos --- posts/infinity-cosmos-announcement.md | 38 +++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 posts/infinity-cosmos-announcement.md diff --git a/posts/infinity-cosmos-announcement.md b/posts/infinity-cosmos-announcement.md new file mode 100644 index 00000000..9f0df116 --- /dev/null +++ b/posts/infinity-cosmos-announcement.md @@ -0,0 +1,38 @@ +--- +author: 'TBD' +category: 'project announcement' +date: 2024-09-10 18:00:00+00:00 +description: '' +has_math: true +link: '' +slug: infinity-cosmos-announcement +tags: '' +title: About +type: text +--- + +[Emily Riehl](https://github.com/emilyriehl) introduces the [∞-Cosmos Project](https://github.com/emilyriehl/infinity-cosmos). + + + +# Introduction + +The term ∞-cosmos refers to an axiomatization of the universe in which ∞-categories live as objects. The axioms are somewhat ad-hoc and chosen for largely pragmatic reasons. In particular, the axioms are stated in the language of 1-category theory and simplicially enriched category theory, rather than in the language of ∞-category theory itself. The notion of ∞-cosmoi enables a "model-independent" development of the theory of ∞-categories, since various models such as quasi-categories and complete Segal spaces assemble into ∞-cosmoi. + +Much of the development of the theory of ∞-categories takes place not in the full ∞-cosmos but in a quotient 2-category whose objects are ∞-categories, whose morphisms are ∞-functors, and whose 2-cells are ∞-natural transformations. We call this the homotopy 2-category since it is a quotient of the ∞-cosmos (which is an (∞,2)-category of a particular form) much like an (∞,1)-category has a quotient homotopy (1-)category. For instance, the existing Mathlib notions of equivalences and adjunctions in a bicategory specialize to define equivalences and adjunctions between ∞-categories when interpreted in the homotopy 2-category. + +# Initial scope + +The initial aims of this project are relatively modest, though with sufficient interest its ambitions could expand considerably. In particular, our initial intention is not to attempt the difficult theorem of proving that the cartesian closed category of quasi-categories defines an example of an ∞-cosmos (among other things, the cartesian closure of this subcategory has not yet been proven) but rather create a large "bounty" to reward anyone who succeeds in this task in the form of a large cache of ∞-categorical theorems that will follow immediately. + +# Team behind ∞-Cosmos + +This project is being co-lead by [Dominic Verity](https://github.com/dom-verity) and [Mario Carneiro](https://github.com/digama0). + + +# Contributing + +We invite everyone to join us at our [channel at the leanprover Zulip](https://leanprover.zulipchat.com/#narrow/stream/455414-Infinity-Cosmos) for discussions and organisation of development. +If you are interested in contributing to ∞-Cosmos, we look forward to you joining our conversations. + +The project is hosted on [github](https://github.com/emilyriehl/infinity-cosmos), including the [overview](https://emilyriehl.github.io/infinity-cosmos/) and [blueprint](https://emilyriehl.github.io/infinity-cosmos/blueprint/). From a7387446e13590da7cf2a9a6a5136c0f63efe3b4 Mon Sep 17 00:00:00 2001 From: Sebastian Englbrecht Date: Tue, 17 Sep 2024 19:57:24 +0200 Subject: [PATCH 2/4] add suggested text to blogpost --- posts/infinity-cosmos-announcement.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/posts/infinity-cosmos-announcement.md b/posts/infinity-cosmos-announcement.md index 9f0df116..b7f42463 100644 --- a/posts/infinity-cosmos-announcement.md +++ b/posts/infinity-cosmos-announcement.md @@ -1,13 +1,13 @@ --- -author: 'TBD' +author: 'Emily Riehl' category: 'project announcement' -date: 2024-09-10 18:00:00+00:00 +date: 2024-09-17 18:00:00+00:00 description: '' has_math: true link: '' slug: infinity-cosmos-announcement -tags: '' -title: About +tags: '∞-Cosmos' +title: Announcing the ∞-Cosmos Project type: text --- @@ -17,22 +17,22 @@ type: text # Introduction -The term ∞-cosmos refers to an axiomatization of the universe in which ∞-categories live as objects. The axioms are somewhat ad-hoc and chosen for largely pragmatic reasons. In particular, the axioms are stated in the language of 1-category theory and simplicially enriched category theory, rather than in the language of ∞-category theory itself. The notion of ∞-cosmoi enables a "model-independent" development of the theory of ∞-categories, since various models such as quasi-categories and complete Segal spaces assemble into ∞-cosmoi. +Now that Lean's category theory library has reached a certain sophistication, it's natural to ask whether it can be extended to a formalization of (at least certain aspects of) (∞,1)-category theory. (∞,1)-categories — often called "[∞-categories](https://www.ams.org/notices/200808/tx080800949p.pdf)" for short — have objects and morphisms, just like ordinary categories, but composition is only defined up to "homotopy" (encoded by the data of a weakly invertible 2-dimensional morphism) and only associative up to still higher "homotopies" (encoded by the data of weakly invertible n-dimensional morphisms, for all natural numbers n). For such a formalization project to be well-founded, it must start from a rigorous definition of ∞-categories — for instance using the presentation of ∞-categories as "[quasi-categories](https://ncatlab.org/nlab/show/quasi-category)," a notion which has been defined in Mathlib — but unfortunately this presentation greatly increases the combinatorial complexity of ∞-categorical definitions and proofs. + +We propose an alternate approach to the formalization of ∞-category theory starting from the axiomatic notion of an [∞-cosmos](https://ncatlab.org/nlab/show/infinity-cosmos). An ∞-cosmos is an axiomatization of the universe in which ∞-categories live as objects. The axioms are somewhat ad-hoc and chosen for largely pragmatic reasons. In particular, the axioms are stated in the language of 1-category theory and simplicially enriched category theory — topics that are well-covered by Mathlib — rather than in the language of ∞-category theory itself. The theory of ∞-cosmoi enables a "model-independent" development of the theory of ∞-categories. On the one hand, various models such as quasi-categories and complete Segal spaces assemble into ∞-cosmoi, so theorems about ∞-categories in an ∞-cosmos apply to the most popular models. At the same time, the ∞-categorical notions developed in an ∞-cosmos are "synthetic" or "formal" as opposed to the original "analytic" definitions, which were typically expressed in the "coordinates" of a particular model. Much of the development of the theory of ∞-categories takes place not in the full ∞-cosmos but in a quotient 2-category whose objects are ∞-categories, whose morphisms are ∞-functors, and whose 2-cells are ∞-natural transformations. We call this the homotopy 2-category since it is a quotient of the ∞-cosmos (which is an (∞,2)-category of a particular form) much like an (∞,1)-category has a quotient homotopy (1-)category. For instance, the existing Mathlib notions of equivalences and adjunctions in a bicategory specialize to define equivalences and adjunctions between ∞-categories when interpreted in the homotopy 2-category. # Initial scope -The initial aims of this project are relatively modest, though with sufficient interest its ambitions could expand considerably. In particular, our initial intention is not to attempt the difficult theorem of proving that the cartesian closed category of quasi-categories defines an example of an ∞-cosmos (among other things, the cartesian closure of this subcategory has not yet been proven) but rather create a large "bounty" to reward anyone who succeeds in this task in the form of a large cache of ∞-categorical theorems that will follow immediately. +The initial aims of this project are relatively modest, though with sufficient interest its ambitions could expand considerably. In particular, our initial intention is not to attempt the difficult theorem of proving that the cartesian closed category of quasi-categories defines an example of an ∞-cosmos; among other things, the cartesian closure of this subcategory has not yet been proven. Instead, our intention is to create a large "bounty" to reward anyone who succeeds in this task in the form of a large cache of ∞-categorical theorems that will follow immediately. # Team behind ∞-Cosmos This project is being co-lead by [Dominic Verity](https://github.com/dom-verity) and [Mario Carneiro](https://github.com/digama0). - # Contributing -We invite everyone to join us at our [channel at the leanprover Zulip](https://leanprover.zulipchat.com/#narrow/stream/455414-Infinity-Cosmos) for discussions and organisation of development. -If you are interested in contributing to ∞-Cosmos, we look forward to you joining our conversations. +We invite everyone to join us at our [channel at the leanprover Zulip](https://leanprover.zulipchat.com/#narrow/stream/455414-Infinity-Cosmos) for discussions and organisation of development. If you are interested in contributing to the ∞-cosmos project, we look forward to you joining our conversations. The project is hosted on [github](https://github.com/emilyriehl/infinity-cosmos), including the [overview](https://emilyriehl.github.io/infinity-cosmos/) and [blueprint](https://emilyriehl.github.io/infinity-cosmos/blueprint/). From 831e382e6af181855d6ca83d2bdca9f9699d401f Mon Sep 17 00:00:00 2001 From: Sebastian Englbrecht Date: Tue, 17 Sep 2024 19:59:47 +0200 Subject: [PATCH 3/4] fix comma --- posts/infinity-cosmos-announcement.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/infinity-cosmos-announcement.md b/posts/infinity-cosmos-announcement.md index b7f42463..6bd759c0 100644 --- a/posts/infinity-cosmos-announcement.md +++ b/posts/infinity-cosmos-announcement.md @@ -17,7 +17,7 @@ type: text # Introduction -Now that Lean's category theory library has reached a certain sophistication, it's natural to ask whether it can be extended to a formalization of (at least certain aspects of) (∞,1)-category theory. (∞,1)-categories — often called "[∞-categories](https://www.ams.org/notices/200808/tx080800949p.pdf)" for short — have objects and morphisms, just like ordinary categories, but composition is only defined up to "homotopy" (encoded by the data of a weakly invertible 2-dimensional morphism) and only associative up to still higher "homotopies" (encoded by the data of weakly invertible n-dimensional morphisms, for all natural numbers n). For such a formalization project to be well-founded, it must start from a rigorous definition of ∞-categories — for instance using the presentation of ∞-categories as "[quasi-categories](https://ncatlab.org/nlab/show/quasi-category)," a notion which has been defined in Mathlib — but unfortunately this presentation greatly increases the combinatorial complexity of ∞-categorical definitions and proofs. +Now that Lean's category theory library has reached a certain sophistication, it's natural to ask whether it can be extended to a formalization of (at least certain aspects of) (∞,1)-category theory. (∞,1)-categories — often called "[∞-categories](https://www.ams.org/notices/200808/tx080800949p.pdf)" for short — have objects and morphisms, just like ordinary categories, but composition is only defined up to "homotopy" (encoded by the data of a weakly invertible 2-dimensional morphism) and only associative up to still higher "homotopies" (encoded by the data of weakly invertible n-dimensional morphisms, for all natural numbers n). For such a formalization project to be well-founded, it must start from a rigorous definition of ∞-categories — for instance using the presentation of ∞-categories as "[quasi-categories](https://ncatlab.org/nlab/show/quasi-category)", a notion which has been defined in Mathlib — but unfortunately this presentation greatly increases the combinatorial complexity of ∞-categorical definitions and proofs. We propose an alternate approach to the formalization of ∞-category theory starting from the axiomatic notion of an [∞-cosmos](https://ncatlab.org/nlab/show/infinity-cosmos). An ∞-cosmos is an axiomatization of the universe in which ∞-categories live as objects. The axioms are somewhat ad-hoc and chosen for largely pragmatic reasons. In particular, the axioms are stated in the language of 1-category theory and simplicially enriched category theory — topics that are well-covered by Mathlib — rather than in the language of ∞-category theory itself. The theory of ∞-cosmoi enables a "model-independent" development of the theory of ∞-categories. On the one hand, various models such as quasi-categories and complete Segal spaces assemble into ∞-cosmoi, so theorems about ∞-categories in an ∞-cosmos apply to the most popular models. At the same time, the ∞-categorical notions developed in an ∞-cosmos are "synthetic" or "formal" as opposed to the original "analytic" definitions, which were typically expressed in the "coordinates" of a particular model. From 0eb91c19f94aa9c4523ff267ae1ef70877761c1c Mon Sep 17 00:00:00 2001 From: Sebastian Englbrecht Date: Tue, 17 Sep 2024 20:42:53 +0200 Subject: [PATCH 4/4] fix team section --- posts/infinity-cosmos-announcement.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/infinity-cosmos-announcement.md b/posts/infinity-cosmos-announcement.md index 6bd759c0..41c85f59 100644 --- a/posts/infinity-cosmos-announcement.md +++ b/posts/infinity-cosmos-announcement.md @@ -29,7 +29,7 @@ The initial aims of this project are relatively modest, though with sufficient i # Team behind ∞-Cosmos -This project is being co-lead by [Dominic Verity](https://github.com/dom-verity) and [Mario Carneiro](https://github.com/digama0). +This project is being co-led by [Mario Carneiro](https://github.com/digama0), [Emily Riehl](https://github.com/emilyriehl), and [Dominic Verity](https://github.com/dom-verity). # Contributing