You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Alex Kavvos (Mar 26 2020 at 16:20):This is the HoTT stream. Welcome!
Mike Shulman (Mar 26 2020 at 18:20):In case anyone is unaware, there is also a dedicated HoTT zulip.
Alex Kavvos (Mar 26 2020 at 21:55):Mike Shulman said:
In case anyone is unaware, there is also a dedicated HoTT zulip.
...which explains the awful silence here.
Christian Williams (Mar 26 2020 at 23:21):that's good. could someone possibly set a link here, for people to join?
Nathanael Arkor (Mar 26 2020 at 23:22): T Murrills (Mar 26 2020 at 23:23):hmmm, it says I'm not a member of that organization when I try to log in. Does an invite link need to be provided or something? (I encountered a similar situation trying to join here; not sure if that's changed.)
Nathanael Arkor (Mar 26 2020 at 23:25):you have to click "Sign up" at the bottom of the page
Nathanael Arkor (Mar 26 2020 at 23:26):it seems to have been started just a few days before this one
T Murrills (Mar 26 2020 at 23:28):ah, ok! sorry, I thought that was for signing up for a zulip account itself. :)
Nathanael Arkor (Mar 26 2020 at 23:30):I agree it's unclear — there are no global Zulip accounts, though, so it's always particular to an organisation
Patrick Nicodemus (Jul 24 2021 at 15:05):Hi all. I am reading about the Steenrod squaring operations today. One of the applications of this idea is as follows. If X is a space, and C(X) denotes the chain complex of singular simplices in X, then there is a natural map T: C(X) -> C(X) \otimes C(X) called the Alexander-Whitney map. We can prove that this is the unique natural map up to homotopy. In particular, we can show that (letting tau denote the symmetry isomorphism in the category of chain complexes) T \simeq \tau T, so this map is co-commutative up to homotopy by some h_0 : T \simeq \tau T. Furthermore it is known that h_0 is homotopic to \tau h_0 by some higher homotopy h_1, and inductively there exists h_{n+1} : h_n\simeq \tau h_n for each n.
The Steenrod squares are certain algebraic invariants in cohomology derived from these higher homotopies. The fact that there are nonzero Steenrod squares shows that these higher homotopies cannot always be the constant homotopy at a point; in particular, we cannot give a natural map f: C(X) -> C(X)\otimes C(X) such that \tau f = f on the nose, because if this were the case then we could always have h_n be the constant homotopy for all n.
My question is how could we state this or express it in homotopy type theory? Intuitively I want to say something like "there is no natural map f: C(X) -> C(X) \otimes C(X) such that tau f = f by the reflexivity proof" but this seems like nonsense. What is being shown is something like that tau f is not definitionally equal or rewrite equal to f in general even though the identity type f = tau f is contractible (?). But we cannot say in HoTT that "A is not definitionally equal to B."
Mike Shulman (Jul 25 2021 at 00:53):The problem is more basic: you can't even define in HoTT.
Leopold Schlicht (Aug 11 2021 at 13:46):What does that mean and how can one prove that one can't define it?
Jake Gillberg (Aug 11 2021 at 15:10):I don’t think there is a proof that it can’t be done, but folks have tried and failed to define simplicial complexes in HoTT. https://hott-uf.github.io/2020/HoTTUF_2020_paper_11.pdf
Mike Shulman (Aug 11 2021 at 17:02):I should have been more clear. Part of the problem is that the question doesn't specify what is to be meant by a "space" or a "chain complex" in HoTT. If by "space" we mean a set equipped with a topology, and by "chain complex" we mean a collection of sets with abelian group structures and differentials between them, then we are just importing ordinary set-based mathematics into HoTT, and we can say all the usual things in the usual way: means on-the-nose equality and if we want something weaker we have to explicitly refer to chain homotopies.
Mike Shulman (Aug 11 2021 at 17:03):If by "space" we mean a type, but by "chain complex" we still mean a collection of sets with abelian group structures and differentials, then it's not known how to define (although we do of course know what a chain complex of this sort is).
Mike Shulman (Aug 11 2021 at 17:05):If instead by "chain complex" we mean some homotopical object built out of higher types that would correspond in the classical model to a chain complex (such as an -module spectrum), then we don't even know how to define that kind of chain complex in HoTT. We can define spectra, but highly structured ring and module spectra are currently out of reach (except, as always with these questions, when using 2LTT).
Mike Shulman (Aug 11 2021 at 17:10):However, I guess it does make sense to ask this question about an imaginary version of the latter situation. If we were using 2LTT then we could indeed say, at the exo-level, that is not exo-equal to . But this would not be an "internal" statement in the fibrant fragment, and you're right that in that world we cannot negate definitional equality. Instead we have to talk about homotopy-invariant statements, such as for instance "there are nonzero Steenrod squares". (-:
Mike Shulman (Aug 11 2021 at 17:13):So I guess the best answer to the original question may be "we can't". (-: