Not signed in (Sign In)

Start a new discussion

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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 31st 2020

    Added a section on terminology.

    diff, v40, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2020

    Seems an odd choice ’anima’. But why would the plural be the same? Thought it was a feminine noun: here, so ’animae’.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2020

    I see here, p. 36:

    If the objects of C are called widgets, then we call those of Ani(C) animated widgets, except that we abbreviate Ani(Set) to Ani and the term ‘animated set’ to anima (plural: anima).


    • CommentRowNumber4.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 31st 2020

    Added a citation.

    diff, v42, current

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2020

    Move terminology section to the end, since some of it is fairly idiosyncratic and shouldn’t be emphasized to a newcomer. Also move the more common usages to the top of the section and add historical comments.

    diff, v43, current

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2020

    I have to say that I am not animated by the terminology “anima”.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2020

    The ideosyncrasy reminds me of the fact that there still is no text that would serve as introducing/communicating homotopy theory to its neighbour fields (think of differential geometers, mathematical physicists, …).

    • CommentRowNumber8.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 31st 2020

    “Anima” has an advantage of being a single short nonhyphenated word without special symbols that is already present in your spellchecker’s dictionary. Only “space” can compete with it, but a lot of people hate “space”.

    Re #7: Not only we do not have a text that introduces modern homotopy theory to its neighbor fields, we also do not have a text that introduces modern homotopy theory to (future) homotopy theorists!

    For example, the only published elementary introduction to simplicial sets is a short survey by Friedman. But it doesn’t go far.

    Goerss and Jardine start by assuming the reader already mastered a textbook like Hatcher or tom Dieck.

    Lurie’s Higher Topos Theory and Cisinski’s Higher Categories and Homotopical Algebra also assume a lot of background.

    Lurie’s Kerodon could become a more accessible source one day.

    • CommentRowNumber9.
    • CommentAuthorTim_Porter
    • CommentTimeMar 31st 2020

    There is the ancient survey article of Curtis on simplicial homotopy theory that does some nice stuff that is often not mentioned.

    To return to this thread, I find the term ‘anima’ without any mental hook to attach it to an infinity groupoid.

    • CommentRowNumber10.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 31st 2020

    The presumed mental hook (as indicated by Scholze) is that Beilinson referred to the process of introducing coherent homotopies (e.g., turning rings into simplicial rings, etc.) as “animating” them.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2020

    Only “space” can compete with it

    What about “type”?

    • CommentRowNumber12.
    • CommentAuthorDmitri Pavlov
    • CommentTimeApr 1st 2020

    Re #11: Doesn’t “type” also refer to types in extensional type theory, which are not at all like homotopy types?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2020

    Those are just the 0-truncated ones. (-:

    • CommentRowNumber14.
    • CommentAuthorUlrik
    • CommentTimeApr 1st 2020

    Trying to fix up the “Relation to infty-groups”-section.

    diff, v44, current

    • CommentRowNumber15.
    • CommentAuthorSam Staton
    • CommentTimeApr 23rd 2020

    Explicitly saying that “anima” is a synonym for infinity groupoid, since this wasn’t explicit in what was there before. I hope this is right! Googling “anima” and “condensed anima” yields pages on psychology and World of Warcraft respectively…

    diff, v45, current

    • CommentRowNumber16.
    • CommentAuthorDmitri Pavlov
    • CommentTimeApr 24th 2020
    • (edited Apr 24th 2020)

    Looks right to me.

    It is really annoying that homotopy theorists cannot settle on a single name, whether it is “space”, “type”, or “anima”.

    I hope this changes soon and all but one terms die out. (I don’t even care that much which one wins.)

    And we also need a shorter name for our profession. How about “homotopists” instead of “homotopy theorists”?

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeApr 24th 2020

    How about “homotopists” instead of “homotopy theorists”?

    The short form should be “type theorists”.

    (The years go by, and what once was the beginning of the bright future of a great new unifying idea is gradually becoming a faint memory of what could have been. Homotopy-Type-Theory, does anyone remember what this was about?)

    • CommentRowNumber18.
    • CommentAuthoratmacen
    • CommentTimeApr 24th 2020

    Re #11, #17:

    The meaning of “type” depends on the situation. Even if the meaning of “type” is always some special case of the homotopy types (and is that even suspected?), that’s still generally a different meaning from the entirety of homotopy types.

    I like to think of myself as a type theorist, and I’m definitely not a homotopy theorist.

    HoTT is great, but let’s not get carried away; type theory and abstract homotopy theory are not the same subject.

    (What was the bright future? Why isn’t it happening? Is it too late?)

    • CommentRowNumber19.
    • CommentAuthorDmitri Pavlov
    • CommentTimeApr 26th 2020

    Re #18: One truly depressing aspect is that we still don’t know how to define (∞,1)-categories in homotopy type theory.

    • CommentRowNumber20.
    • CommentAuthoratmacen
    • CommentTimeApr 27th 2020

    Yeah, and I think part of that is that you need coherence conditions at all dimensions, and nobody knows how to do that in most versions of HoTT. I think that problem is really interesting. I’m hoping there’s a sneaky way to do it already in Book HoTT, but it seems like most people think it can’t be done in Book HoTT. Given that, I’d have thought people would be trying to reach a consensus on what system to use instead, but it looks like they aren’t. They’re trying many different systems, and—it seems—not focusing on the ability to solve coherence problems.

    • CommentRowNumber21.
    • CommentAuthorHurkyl
    • CommentTimeApr 27th 2020
    • (edited Apr 27th 2020)

    I suppose I’m expressing my ignorance, but I thought the idea for (∞,1)-categories was via (infinity) precategories – functors P:Δ opTypeP : \Delta^\mathrm{op} \to \mathrm{Type} such that P(Δ n)P(\Delta^n) is the type of nn-long strings of composable arrows. Then the (∞,1)-categories would be the one where the degeneracy P(Δ 0)P(Δ 1)P(\Delta^0) \to P(\Delta^1) is an equivalence with the subtype of invertible arrows.

    Is the problem that we don’t know how to formalize Type-valued functors out of a 1-category? Or something else?

    • CommentRowNumber22.
    • CommentAuthorDmitri Pavlov
    • CommentTimeApr 27th 2020

    Re #21: If I understand it correctly, once we can define simplicial types (i.e., simplicial ∞-groupoids), then we know how to proceed to define (∞,1)-categories using Segal-type constructions.

    However, a simplicial type is (or should be) a functor X:Δ opTypeX\colon\Delta^op \to Type, and it is not at all clear how to encode all coherences here: for each [n]Δ op[n]\in\Delta^op we have a type X nX_n, for each a:[m][n]a\colon[m]\to[n] we have a map X a:X nX mX_a\colon X_n\to X_m, for each a:[l][m]a\colon[l]\to[m] and b:[m][n]b\colon[m]\to[n] we have X a,b:X bX a=X baX_{a,b}:X_b\circ X_a = X_{b\circ a}, and it seems like there is no easy way to encode all these in HoTT.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 19th 2020

    I have no idea what Urs is talking about in #17. It sounds like maybe the real world failed to live up to exaggerated expectations in some way?

    Trying many different systems is part of the process of reaching a consensus on which is the best. Currently the most promising type theory for solving general coherence problems is some form of “2-level type theory”, but uptake of that has been slow, probably partly due to its arguably unaesthetic nature, partly to its not having been implemented directly in a proof assistant, partly due to hopes that something better will be found, and partly due to most people in the field having plenty of other problems to keep them busy that don’t require infinite coherence.

    • CommentRowNumber24.
    • CommentAuthorCharles Rezk
    • CommentTimeFeb 23rd 2021

    Re #7, #8: So what should a text (introducing/communicating homotopy theory to the masses) contain? If I knew what is supposed to be in it I might try to write it.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeFeb 23rd 2021

    Hi Charles,

    thanks for the message. Here some quick thoughts. Maybe to be followed up later when I am more awake.

    Most importantly, it must Not start with talking about simplical categories or anything remotely like that. The audience in #7 has no idea what this means.

    It’s not just that they don’t know the technical details (this audience is able to appreciate theory while glossing over details) but they have no idea what to make of such words at all.

    The audience in #7 is typically used to seeing fairly sophisticated aspects of dg-homotopy theory, though not under that name.

    These people often have religious feelings towards the equation dd=0d \circ d = 0. One could start by explaining how the simplicial identities generalize this homological “master equation”.

    Hence besides briefly recalling elements of point-set topological homotopy, an introduction for them should probably motivate homotopy theory as the “non-abelian generalization” of homological algebra. Dold-Kan as the road to homotopy theory.

    Derived categories might be an excellent point of contact, and motivating examples should be given in the context of complex-analytic/algebraic geometry.

    (Yes, I think this audience may tend to have an easier time connecting to derived categories than to plain categories, much like many people think they know operads only in chain complexes. At least they all have heard of applications of derived categories, but will mostly never heard of a sensible application of a plain category.)

    Just some quick thoughts. Maybe more later.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJul 27th 2021

    This entry was (and is) lacking references. I have now, at least, added pointer to:

    diff, v47, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)