Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I always found that the formulation of the theory of infinity-algebras over an (infinity,1)-operad in Lurie’s Higher Algebra nicely captures what Baez-Dolan called the microcosm principle.
I have added a corresponding remark to the latter entry and expanded slightly.
I still think that the principle holds much more generally than the case from the Lurie’s work. It is not only about algebraic structures in the narrow, operadic, sense, but even beyond algebraic. And not only for (special cases of) $(\infty,1)$-categories but also for multicategories, $(n,k)$-categories etc. etc.
Certainly there will be an analogous principle for more general higher categories.
But do you know of a formalization that accomplishes it? Or are you just saying that in the future there will be one?
I think it is a heuristics, and each heuristics has some special cases which can be formalized. I do not believe that there will be ever a formulation which will include all instances of heuristics and do not think it would be even good to identify the formalization of one very large family of cases of a heuristics with heuristics itself. Each such formalization is an exercise or an application of a heuristics and it should be considered only as an application. Even when it covers lots of important cases and is mathematically of course very interesting. I think we should present the Lurie’s case not as a formulation of the general principle, but as one of the big instances/applications where it works.
I think we should present the Lurie’s case not as a formulation of the general principle, but as one of the big instances/applications where it works.
Currently it says in the entry “a formalization … in the context of $(\infty,1)$-category theory”. That seems perfectly accurate to me. Notice that this is vastly more general already than what Baez-Dolan had considered.
But feel invited to add further remarks to the entry.
“a formalization … in the context of (∞,1)-category theory”
In my reading, this is suggesting quite strongly that there are no other important cases of microcosm principle in the context of (∞,1)-category theory, what is certainly not true. Generalizations to other kinds of categories is one thing, but the generalizations to structures different than algebras over operads is another. The second restriction is here crucial, and my reading of Baez-Dolan would be to go beyond those. I will think of some examples later.
A but different but similar issue/example. Rosenberg discovered for algebraic K-theory that a more general setup than Quillen model categories are right ’exact’ categories in his sense; these are categories equipped with subcanonical singleton Grothendieck topology; now the derived functors can be defined in left and right ’exact’ categories. The category of all right exact small categories is a left ’exact’ category in his sense. This makes general K-theory possible: the objects are right ’exact’ categories and one can do derived functors within the world in which they live and for right choice of global sections one gets a universal K-theory. This is a bit different than the instance of Baez-Dolan – one does not need left exact microcosmos to define within right exact structure. But on the other hand, the left exact comes from collection of all right exact ones, so the situation that the natural structure of the same type is on the container of all of them is also true. I know it is not quite Baez-Dolan.
I know of another example with what I call hierarchy of distributive laws, how $n$-categorical come from algebras over things which have $(n+1)$-categorical distributive laws to be made compatible, but it is a bit lengthy to explain.
I don’t understand what you are saying, sorry.
One evident point where one could conceivably generalize is to observe that there are $\infty$-algebras over some $\infty$-monad which are not $\infty$-algebras over some $\infty$-operad. So a more general formalization in the context of $(\infty,1)$-categories would be to pass to algebraic structures defined by $\infty$-monads.
I’ve encountered two instances of the microcosm principle which I have no idea how to express in operadic or even monadic language. The first is that in order to define a notion of trace for 2-morphisms in a bicategory, you need the bicategory to be equipped with a categorified trace. The second is that in order to express the universal property of the equipment of enriched categories, you need to work in the context of the higher equipment of enriched bicategories.
I added to microcosm principle a mention of the fact that often an internal X in a categorified X is the same as a lax morphism out of the terminal categorified X.
I added to microcosm principle a list of examples (probably incomplete) and some discussion of other formalizations in the literature.
For the moment I made adjoint type theory redirect to the entry presently titled adjoint logic.
I’d be interested in seeing what you have in mind with the last bullet item:
type theories can be defined relative to any “2-type theory”
Yes, I noticed that earlier and was going to ask the same thing.
Ah right, we already had adjoint logic.
What I meant is that in my papers with Dan and his student Mitchell, the data parametrizing an “adjoint type theory” is a 2-category or a 2-multicategory, which is a categorified version of the same structure that the (adjoint) type theory is presenting (a kind of category or multicategory). Moreover, we describe that 2-category or 2-multicategory using its own type theory, and “pun” the variable names for types and their modes. So for instance if a mode $p$ has a tensor product $\otimes$ indicating that its types have linear multiplicative structure, then the multiplicative conjunction of two types $A,B$ in that mode is written $x:A, y:B \vdash_{x\otimes y} \langle x,y\rangle : A\otimes B$; the “mode term” $x:p, y:p\vdash x\otimes y:p$, using the same variables, subscripts the type term judgment to indicate that in the term $\langle x,y\rangle$ we are allowed/required to use the variables $x$ and $y$ once each.
Shall we start a new entry then for 2-type theory, or are you happy with it all directing to adjoint logic? Where to put
Will it be possible to represent dependent type theories in that framework?
Spamming the nForum now! Can that really be worth it? #18 is just a reduced version of #11, by some travel company.
I’ve seen aryavritindia before, with a similarly useless comment here. Probably worth blocking that address.
Probably worth blocking that address.
Yes. We should contact Adeel (by private email, he might not see it here).
Let’s keep it at adjoint logic for now, we can add that citation there too. The dependent version is work in progress.
At MPI Bonn last year, Eric Finster in his talk (here) had some intriguing remarks on how dependent type theory would be implemented in “opetopic type theory” via adjunctions.
He had slides for this, but now I don’t find them online. And probably it’s unrelated.
1 to 23 of 23