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.
Patrick Nicodemus (Feb 20 2024 at 22:37):We have some general theories of categorification, for example opetopes seem to provide a general framework for categorification as the slice construction for opetopes automatically gives you these notions of relations between relations. There are many definitions of higher category. Recently in a related thread someone posted Garner's "Homomorphisms of higher categories" paper which gives a general technique to categorify strict functors to give definitions of weak functors between higher categories.
Do any of these theories of categorification have any associated theorems about categorification of theorems? I.e. if A is the original theory and A' is the categorified theory, some limited fragment of the theory of A is directly translatable to the A' theory, where equalities are weakened to isomorphisms. Are there any such systematic ways of proving that results holding for lower categories hold for higher categories appropriately weakened?
James Deikun (Feb 21 2024 at 00:59):I think there are a few transfer theorems like that in homotopy theory but even there they end up doing most of the work the hard way. Proving results in homotopy type theory (or rather, if you really want a "transfer theorem", intensional Martin-Lof type theory without Axiom K) is the most powerful method I know of off the top.
James Deikun (Feb 21 2024 at 01:13):It's almost impossible (read: usually actually impossible) to do with theorems as statements without looking at the proof at all because those equalities you were using and throwing away in classical proofs now have content and often to even get the statement you really want there are actual things to be proven about them. Proofs as mathematical objects often contain enough information to recover what you need, but just the fact that they're true almost never does.
James Deikun (Feb 21 2024 at 01:25):The most efficient thing you can do is to work in a fragment of logic which is powerful enough that you can prove the classical theorem with a classical proof, but weak enough that it can only prove theorems whose "space of truth values" is (-1)-truncated in the categorified world. (Maybe it can do other constructions, but has a way to separate them syntactically from theorems.) Then you kind of don't need to know what the proof is, just that it was done in that fragment. The problem with this is that traditional (pre-Univalent Foundations) mathematical logic outside of some obscure corners didn't really concern itself with most of the fragments of interest for this. I think a lot of the classical algebraic topologists' interest in operads was exactly concerned with this, so you might want to look into that area.
Patrick Nicodemus (Feb 23 2024 at 19:20):This is a really good point by the way, thanks for the observation. I agree that certainly the proof itself should be what lifts to the higher setting.
Brendan Murphy (Feb 24 2024 at 00:23):Have you seen this paper? https://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf