Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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.

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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) (,1)(\infty,1)-categories but also for multicategories, (n,k)(n,k)-categories etc. etc.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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?

    • CommentRowNumber4.
    • CommentAuthorzskoda
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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 (,1)(\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.

    • CommentRowNumber6.
    • CommentAuthorzskoda
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    “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.

    • CommentRowNumber7.
    • CommentAuthorzskoda
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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 nn-categorical come from algebras over things which have (n+1)(n+1)-categorical distributive laws to be made compatible, but it is a bit lengthy to explain.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2013
    • (edited Feb 11th 2013)

    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 (,1)(\infty,1)-categories would be to pass to algebraic structures defined by \infty-monads.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2013

    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.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 21st 2017

    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.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJun 12th 2017

    I added to microcosm principle a list of examples (probably incomplete) and some discussion of other formalizations in the literature.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 12th 2017

    For the moment I made adjoint type theory redirect to the entry presently titled adjoint logic.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 12th 2017
    • (edited Jun 12th 2017)

    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”

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 12th 2017

    Yes, I noticed that earlier and was going to ask the same thing.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2017

    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 pp has a tensor product \otimes indicating that its types have linear multiplicative structure, then the multiplicative conjunction of two types A,BA,B in that mode is written x:A,y:B xyx,y:ABx:A, y:B \vdash_{x\otimes y} \langle x,y\rangle : A\otimes B; the “mode term” x:p,y:pxy:px:p, y:p\vdash x\otimes y:p, using the same variables, subscripts the type term judgment to indicate that in the term x,y\langle x,y\rangle we are allowed/required to use the variables xx and yy once each.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 13th 2017

    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

    • Daniel Licata, Michael Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), (pdf)?
    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 13th 2017

    Will it be possible to represent dependent type theories in that framework?

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 13th 2017

    Spamming the nForum now! Can that really be worth it? #18 is just a reduced version of #11, by some travel company.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 13th 2017

    I’ve seen aryavritindia before, with a similarly useless comment here. Probably worth blocking that address.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2017

    Probably worth blocking that address.

    Yes. We should contact Adeel (by private email, he might not see it here).

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2017

    Let’s keep it at adjoint logic for now, we can add that citation there too. The dependent version is work in progress.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2017

    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.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2021

    In view of the discussion over here on necessity and sufficiency, should we modify

    Microcosm principle: Certain algebraic structures can be defined in any category equipped with a categorified version of the same structure.

    to something like

    Microcosm principle: Certain algebraic structures can be defined in a (higher) category precisely when it is equipped with a categorified version of the same structure?

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2021

    I don’t know about the original formulation of the principle, but I think this is what is the case in Lurie’s realization of it (here).

    And it makes sense: In order to phase a condition on how an algebraic operation is to behave under commuting two elements, we first have to be able to commute the symbols for these elements.

    But I want to say that I never worked on this and am busy elsewhere and don’t want to be speaking with much authority on the matter.