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 bundle bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex 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 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 homology homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory itex k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar 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 tqft 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.

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)