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.
Jonathan Beardsley (Mar 27 2020 at 21:16):What is a dependent multicategory or dependent operad? I've seen this in a few places on this chat, and I haven't the slightest idea what "dependent" is supposed to mean in this context. Dependent on what?
Nathanael Arkor (Mar 27 2020 at 21:22):cartesian operads model algebraic theories, à la universal algebra
Nathanael Arkor (Mar 27 2020 at 21:22):other notions of operads correspond to other notions of algebraic theory (e.g. symmetric operads correspond to linear algebraic theories)
Jonathan Beardsley (Mar 27 2020 at 21:22):so "cartesian operad" here means Lawvere theory?
Nathanael Arkor (Mar 27 2020 at 21:22):it is equivalent to a Lawvere theory, yes
Jonathan Beardsley (Mar 27 2020 at 21:23):Got it.
Nathanael Arkor (Mar 27 2020 at 21:23):there is desire for a notion of "dependent operad" that captures dependent algebraic theories (à la generalised algebraic theory or essentially algebraic theory)
Nathanael Arkor (Mar 27 2020 at 21:24):whether a definition exists yet is up for debate, but it certainly hasn't been worked out in detail yet
Jonathan Beardsley (Mar 27 2020 at 21:24):ah okay. right so I guess that's where i'm stymied, because I don't know what "dependent algebraic theories" are, or really even "linear algebraic theories."
Nathanael Arkor (Mar 27 2020 at 21:24):linear algebraic theories have a few different names, but they refer to algebraic theories that are presented by equations in which each variable appears on either side of an equation exactly once
Jonathan Beardsley (Mar 27 2020 at 21:25):I see, hence the whole "there is no operad of groups" thing
Nathanael Arkor (Mar 27 2020 at 21:25):right
Nathanael Arkor (Mar 27 2020 at 21:26):there's not one definition of "dependent algebraic theories", but I think @Chaitanya Leena Subramaniam and I have generally been referring to generalised algebraic theories in this context
Jonathan Beardsley (Mar 27 2020 at 21:26):okay cool. is there a paper with a good definition of "generalized algebraic theory"?
Nathanael Arkor (Mar 27 2020 at 21:26):no
Nathanael Arkor (Mar 27 2020 at 21:26):unless you like wading through concrete syntax :)
Nathanael Arkor (Mar 27 2020 at 21:27):the standard reference is still the original paper Generalised algebraic theories and contextual categories (https://www.sciencedirect.com/science/article/pii/0168007286900539)
Nathanael Arkor (Mar 27 2020 at 21:28):it gives some reasonable intuition, but the formal definition leaves a lot to be desired
Nathanael Arkor (Mar 27 2020 at 21:28):the examples there should help give an idea of the sorts of structures that are possible to express in it, though
John Baez (Mar 27 2020 at 22:53):I was stumped by "linear algebraic theory" for a minute, but from context I guess it's an algebraic theory where all the equational laws have a special form: each variable appears exactly once on each side of the equation. For example monoids are described by a linear algebraic theory, but groups are not because the law has twice on side and not at all on the other.
Linear algebraic theories are precisely the algebraic theories whose algebras can also be described by symmetric (colored) operads.
In other words, there's a nice functor from the category of symmetric operads to the category of algebraic theories, and objects in its essential image are linear algebraic theories.
That's my guess.
John Baez (Mar 27 2020 at 22:53):Okay - I see I'm late to the conversation as usual.
Nathanael Arkor (Mar 27 2020 at 22:54):Nathanael Arkor said:
linear algebraic theories have a few different names, but they refer to algebraic theories that are presented by equations in which each variable appears on either side of an equation exactly once
@John Baez: yep; I clarified here
Nathanael Arkor (Mar 27 2020 at 22:54):I've heard other names for them, but they're really unsuggestive to me
Nathanael Arkor (Mar 27 2020 at 22:54):from a type theoretic perspective, "linear" is very suggestive, though
Nathanael Arkor (Mar 27 2020 at 22:57):"strongly regular algebraic theory" describes those corresponding to (planar) operads, for instance, but "ordered algebraic theory" again seems more natural
Nathanael Arkor (Mar 27 2020 at 22:57):I think "regular" is another name for "linear"
Jonathan Beardsley (Mar 27 2020 at 23:59):@Nathanael Arkor do you know if there's anything useful on the algebraic theory side associated to semi-cartesian operads?
Jonathan Beardsley (Mar 28 2020 at 00:00):Also are you familiar with the "category of operators" associated to a multicategory?
Nathanael Arkor (Mar 28 2020 at 00:11):@Jonathan Beardsley: semi-cartesian operads would correspond to what I would call "affine algebraic theories", as they're structures that you could describe using a form of affine logic (in comparison to linear logic for symmetric operads), but I imagine algebraicists have a different name for these if they've even been specifically studied
Jonathan Beardsley (Mar 28 2020 at 00:13):From what I can tell they have not been studied really
Nathanael Arkor (Mar 28 2020 at 00:19):there should be a notion of "relevance operad" corresponding to relevant monoidal categories and relevant logic, but I can't find reference to one now (it may just have a completely different name)
Nathanael Arkor (Mar 28 2020 at 00:19):it would be nice to have a table with all the different names for these structures, coming from different fields
Nathanael Arkor (Mar 28 2020 at 00:20):I think there's typically been less interest in allowing only one of weakening or contraction — usually one goes straight from linear theories to algebraic theories from what I've seen
Nathanael Arkor (Mar 28 2020 at 00:21):Also are you familiar with the "category of operators" associated to a multicategory?
I've read about this construction before, but I'm not very familiar with it
Nathanael Arkor (Mar 28 2020 at 00:23):ah, I think I read the nLab post on it
Nathanael Arkor (Mar 28 2020 at 00:31):I don't quite see now why the category of operators is canonical, and why we couldn't do something similar with a different sort of operad than semicartesian
Jonathan Beardsley (Mar 28 2020 at 01:23):Oh sure, it's just that it had been used historically. You could do it with anything.
Jonathan Beardsley (Mar 28 2020 at 17:09):Okay, so here's a sort of silly question, since I really don't understand "generalized algebraic theories" at all, but it seems like one of the basic ideas is that the "sorts" are themselves an algebraic type (rather than just a set). So what happens if you do the silly thing of defining something like an "internal theory" to something like the category of theories?
Nathanael Arkor (Mar 28 2020 at 17:37):you can certainly describe other kinds of theories using generalised algebraic theories, if that's what you mean
Nathanael Arkor (Mar 28 2020 at 17:37):e.g. you can describe essentially algebraic theories as a generalised algebraic theory, whose models will then coincide with the models for essentially algebraic theories in the classical sense
Nathanael Arkor (Mar 28 2020 at 17:37):is that what you meant?
Jonathan Beardsley (Mar 28 2020 at 17:38):No so I mean, take some definition like this: image.png
Nathanael Arkor (Mar 28 2020 at 17:38):or you mean something like "monoid in a monoidal category", but "generalised algebraic theory in a categorified generalised algebraic theory"?
Jonathan Beardsley (Mar 28 2020 at 17:39):And then replace "set of sort S" with something that isn't a set.
Jonathan Beardsley (Mar 28 2020 at 17:39):Yes, something more like the latter thing.
Nathanael Arkor (Mar 28 2020 at 17:41):I've seen people look at models of one theory inside a category of models of another, but not models of a theory inside the category of theories
Nathanael Arkor (Mar 28 2020 at 17:42):I'm not quite sure what that would look like
Nathanael Arkor (Mar 28 2020 at 17:43):though it's surely possible, because the category of generalised algebraic theories has good structure — for example, it's locally finitely presentable
Nathanael Arkor (Mar 28 2020 at 17:45):it seems simpler to ask a related question about algebraic theories: e.g. what does a group internal to the category of Lawvere theories look like?
John Baez (Mar 28 2020 at 19:29):A group internal to the category of Lawvere theories is the same as a Lawvere theory internal to the category of groups, so if I'm not screwing up it's Lawvere theory where for each pair of natural numbers m,n there's a group of operations hom(m,n), and composition homomorphisms hom(m,n) hom(n,o) hom(m,o)\times$$ hom(m',n') hom(m+m',n+n'), etc.
Nathanael Arkor (Mar 28 2020 at 19:34):@John Baez: that's a better perspective to view it from :+1:
Nathanael Arkor (Mar 28 2020 at 19:35):are "internal Lawvere theories" studied very often? I don't think I've come across them before
John Baez (Mar 28 2020 at 19:35):Thanks!
John Baez (Mar 28 2020 at 19:37):I've never heard about them. But I know that Lawvere theories are models of a multisorted Lawvere theory. Once you know this, you can look at Lawvere theories in any category with finite products, and know a bunch of stuff is true about them.
What I just did was use "commutativity of internalization". If you've got (multisorted) Lawvere theories X and Y, a model of X in the category of models of Y is a model of Y in the category of models of X.
Jonathan Beardsley (Mar 29 2020 at 00:46):Right. All I was saying is that a GAT is something like an "algebraic theory whose 'set of colors' is itself an algebraic theory," which seemed like it might be formalizable as some kind of double algebraic theory
Jonathan Beardsley (Mar 29 2020 at 00:46):In the same way that we can think of a category internal to as having a space of objects.
Nathanael Arkor (Mar 29 2020 at 00:53):I would think of a theory that had a theory of colours being more like a simple type theory, where we have algebraic structure on the types, e.g. products
Nathanael Arkor (Mar 29 2020 at 00:54):a GAT does have more structure on its collection of sorts, but it's not quite algebraic
Nathanael Arkor (Mar 29 2020 at 00:54):it's categorical, but generally not that structured
Nathanael Arkor (Mar 29 2020 at 01:00):where we have algebraic structure on the types, e.g. products
actually, this is if we had a model of a theory as the colours, rather than the theory itself, so this isn't quite right
Nathanael Arkor (Mar 29 2020 at 01:10):Right. All I was saying is that a GAT is something like an "algebraic theory whose 'set of colors' is itself an algebraic theory,"
I'll think about this in more detail when I'm a little more awake
Jonathan Beardsley (Mar 29 2020 at 02:21):reading a bit more about GATs
Jonathan Beardsley (Mar 29 2020 at 02:21):they're pretty cool
Jonathan Beardsley (Mar 29 2020 at 02:21):the GAT of categories seems like a useful example
Jonathan Beardsley (Mar 29 2020 at 02:22):it's weird for me, because I'm pretty used to thinking about parameterized things (e.g. parameterized homotopy theory) but say the word "dependent type" and I get very anxious. But it seems like it's just, sort of, allowing for "parameterized types."
Jonathan Beardsley (Mar 29 2020 at 02:27):But I suppose I don't entirely yet understand how to think of an operad as an "algebraic theory." So maybe I need to crack that open a bit to get a sense of what a "dependent operad" might look like.
Jonathan Beardsley (Mar 29 2020 at 02:35):But so here's a possibly silly question: given a GAT that has dependent types as possible inputs to operations, it seems possible that one could, instead, just list all possible types (enumerated over all possible indexing types) and then write down an infinite list of rules, thereby getting a single theory (albeit with an infinite list of types and rules). Am I misunderstanding something by saying this?
Christian Williams (Mar 29 2020 at 02:37):I'm reading about them too. I thought a GAT was just another term for "finite limits theory" (I thought GATs and EATs were the same), and now I see they're different! but you can describe the theory of categories either way. apparently the two are actually equivalent.
Jonathan Beardsley (Mar 29 2020 at 02:37):Yeah I saw that as well.
Jonathan Beardsley (Mar 29 2020 at 02:38):Okay essentially algebraic theories are the same as finite limit theories?
Christian Williams (Mar 29 2020 at 02:39):yes.
Jonathan Beardsley (Mar 29 2020 at 02:39):I see
Jonathan Beardsley (Mar 29 2020 at 02:41):Okay so I'm thinking about the following thing:
Jonathan Beardsley (Mar 29 2020 at 02:41):
Jonathan Beardsley (Mar 29 2020 at 02:42):so there's sort of a two-column dictionary happening here
Jonathan Beardsley (Mar 29 2020 at 02:45):
Jonathan Beardsley (Mar 29 2020 at 02:46):apologies for my terrible handwriting (i'm writing on an upright screen, haha)
Jonathan Beardsley (Mar 29 2020 at 02:46):and there should be a third column
Jonathan Beardsley (Mar 29 2020 at 02:46):let me fill in a few things
Nathanael Arkor (Mar 29 2020 at 02:47):apparently the two are actually equivalent.
their models in are equivalent
Nathanael Arkor (Mar 29 2020 at 02:48):I don't think they're equivalent in all settings
Christian Williams (Mar 29 2020 at 02:48):we could call this "Morita equivalence", right?
Nathanael Arkor (Mar 29 2020 at 02:48):But it seems like it's just, sort of, allowing for "parameterized types."
yes, (term-)parameterised types are a reasonable way to think of dependent types
Nathanael Arkor (Mar 29 2020 at 02:49):we could call this "Morita equivalence", right?
that's how I've been thinking of them, yes, though it's a meta-level higher than Morita equivalence is usually considered
Jonathan Beardsley (Mar 29 2020 at 02:51):
Nathanael Arkor (Mar 29 2020 at 02:51):yes
Jonathan Beardsley (Mar 29 2020 at 02:52):and I'm not entirely sure how EATs fit into the picture
Jonathan Beardsley (Mar 29 2020 at 02:52):(deleted)
Nathanael Arkor (Mar 29 2020 at 02:53):Jonathan Beardsley said:
But so here's a possibly silly question: given a GAT that has dependent types as possible inputs to operations, it seems possible that one could, instead, just list all possible types (enumerated over all possible indexing types) and then write down an infinite list of rules, thereby getting a single theory (albeit with an infinite list of types and rules). Am I misunderstanding something by saying this?
I think you could do this, but I don't think the models for this theory would be the same as the models for the GAT
Nathanael Arkor (Mar 29 2020 at 02:53):because models for algebraic theories just have to be product-preserving, i.e. preserve algebraic structure
Nathanael Arkor (Mar 29 2020 at 02:53):but for GATs, you want to preserve more structure than that, i.e. the dependent structure
Jonathan Beardsley (Mar 29 2020 at 02:54):aha, yeah you want to remember what depended on what
Jonathan Beardsley (Mar 29 2020 at 02:54):interesting
Jonathan Beardsley (Mar 29 2020 at 02:54):@Nathanael Arkor do you have a good reference for seeing the relationship between (symmetric) multicategories and linear algebraic theories?
Nathanael Arkor (Mar 29 2020 at 02:54):Jonathan Beardsley said:
and I'm not entirely sure how EATs fit into the picture
in the two rightmost columns, you have "finitely complete categories" and "essentially algebraic theories"
Jonathan Beardsley (Mar 29 2020 at 02:54):aha
Nathanael Arkor (Mar 29 2020 at 02:55):the reference that immediately comes to mind is https://arxiv.org/pdf/1002.0879.pdf
Nathanael Arkor (Mar 29 2020 at 02:55):I'm not sure if it's the best introduction
Jonathan Beardsley (Mar 29 2020 at 02:55):oh well good though, it's a thesis, so hopefully it will be a bit more explanatory than usual
Nathanael Arkor (Mar 29 2020 at 02:56):maybe a better way is to look at the relationship between cartesian multicategories and algebraic theories, and from there, it's easy to see that dropping the weakening and contraction maps in a cartesian multicategory gives you a symmetric multicategory, and this corresponds to ensuring that equations in the theories have the same number of variables on both sides
Nathanael Arkor (Mar 29 2020 at 02:58):https://mikeshulman.github.io/catlog/catlog.pdf is very thorough as well, so I would imagine this also contains a description of the correspondence
Nathanael Arkor (Mar 29 2020 at 02:58):in the two rightmost columns, you have "finitely complete categories" and "essentially algebraic theories"
and I suppose the lefthand column is what we were discussing :)
Nathanael Arkor (Mar 29 2020 at 02:59):GATs and EATs are very similarly structured, so having an operad for one would probably indicate what an operad for the other should look like
Jonathan Beardsley (Mar 29 2020 at 03:01):Nathanael Arkor said:
in the two rightmost columns, you have "finitely complete categories" and "essentially algebraic theories"
and I suppose the lefthand column is what we were discussing :)
yes! very interested in what this lefthand column should be. do we know what the middle column is for GATs?
Nathanael Arkor (Mar 29 2020 at 03:02):well, arguably you could take contextual categories/C-systems, but I think this is a bit unsatisfactory
Jonathan Beardsley (Mar 29 2020 at 03:07):so, reading this page https://ncatlab.org/nlab/show/categorical+model+of+dependent+types
and they say how the issue is that type substitution is strictly associative, but pullback is not, and so they mess with the categories to make this better. however, i think it's the types that need to be fixed, not the categories.
Jonathan Beardsley (Mar 29 2020 at 03:08):perhaps this is somehow dealt with by HoTT
Nathanael Arkor (Mar 29 2020 at 03:09):there have been quite a few papers dealing with the coherence problem of substitution in dependent type theories
Jonathan Beardsley (Mar 29 2020 at 03:09):yeah, sp o
Jonathan Beardsley (Mar 29 2020 at 03:09):good lord i cannot type tonight
Jonathan Beardsley (Mar 29 2020 at 03:10):*yeah so i'm seeing
Nathanael Arkor (Mar 29 2020 at 03:10):The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (https://arxiv.org/pdf/1112.3456.pdf) is maybe the most modern?
Jonathan Beardsley (Mar 29 2020 at 03:13):there's also this: https://arxiv.org/pdf/1211.2851.pdf
Jonathan Beardsley (Mar 29 2020 at 03:13):specifically section 1.2, and Appendix B (according to the nlab)
Jonathan Beardsley (Mar 29 2020 at 03:21):It seems to me that this difference is somehow at the heart of the univalence axiom.
Nathanael Arkor (Mar 29 2020 at 03:31):I'm not familiar enough to give any sort of opinion on that, but I'd be very interested to see a connection
Jonathan Beardsley (Mar 29 2020 at 03:31):well the univalence axiom, very crudely stated by a naif is "equivalence should behave like equality"
Jonathan Beardsley (Mar 29 2020 at 03:32):and the basic issue with pullbacks is that the two ways of pulling back are not equal, they're "equivalent" (in this case, isomorphic)
Nathanael Arkor (Mar 29 2020 at 03:32):that sounds like any sort of coherence result, e.g. monoidal coherence
Nathanael Arkor (Mar 29 2020 at 03:33):is there a link between univalence and coherence theorems?
Jonathan Beardsley (Mar 29 2020 at 03:33):Hm.
Jonathan Beardsley (Mar 29 2020 at 03:34):Well, okay so it's not quite a coherence type thing.
Jonathan Beardsley (Mar 29 2020 at 03:35):The issue being that when you pass to the world in which you're doing something like the Univalence Axiom... it's like... "equality" doesn't exist anymore
Jonathan Beardsley (Mar 29 2020 at 03:35):I don't really understand it.
Jonathan Beardsley (Mar 29 2020 at 03:35):I mean, I guess I don't really understand the Univalence Axiom, like what it's actually saying.
Jonathan Beardsley (Mar 29 2020 at 03:37):like, stupid question: in intensional type theory, can we say that two things (terms? propositions? types?) are equal?
Jonathan Beardsley (Mar 29 2020 at 03:37):I don't really know what the "things" are called whose equality we're checking
Nathanael Arkor (Mar 29 2020 at 03:38):yes, but you have two kinds of equality on terms, so you need to specify which
Nathanael Arkor (Mar 29 2020 at 03:38):terms can be propositionally (i.e. intensionally) equal, or definitionally (i.e. extensionally) equal
Jonathan Beardsley (Mar 29 2020 at 03:38):i see. so there's like "definitional equality" and..
Jonathan Beardsley (Mar 29 2020 at 03:38):okay right
Nathanael Arkor (Mar 29 2020 at 03:40):(anyway, I think I ought to get some sleep now, especially with the clocks changing — I'll catch up on the conversation tomorrow)
Jonathan Beardsley (Mar 29 2020 at 03:41):bye!
Thibaut Benjamin (Apr 07 2020 at 09:33):Seems like I am really late, but I am extremely interested in this discussion, and I have thought a lot about these kinds of things, so here is my take on it:
I want to point out that C-systems/contextual categories can be very (very) wild categorically. You don't even need much for that, it suffices to try and describe -types - they don't come naturally as a limit of anything. The reason being that in the introduction rule
there is one premise which uses $\Gamma$ and one premise which uses $\Gamma,x:A$. Limits in category theory are defined as cones (ie a family of maps starting from the same object), which doesn't match well again these two defferent premises.
Finally I want to ask : in the dependent case, I know essentially of two ways of doing things. The first is the $T$-operads for a monad $T$ (cf Leinster, Higher operads, higher catetgories), and the second is Lawvere theories with arities (cf Berger-Melliès-Weber). Do you know where these fit in this picture? It looks to me like Lawvere theories with arities are analoguous for the cartesian case, since the condition of preserving the nerve functor says things about generic objects being limits of arities, but I don't know of any notion of "dependent cartesian operad". As for $T$-operads, they seem way more general, and at least the monoidal and symmetric monoidal cases are included as special cases, but I don't have any more on that. If you have ideas on these questions, I'd be very interested
Nathanael Arkor (Apr 07 2020 at 11:29):I think one of the questions we were interested in was whether you could use -operads/multicategories for dependency; in some simple cases (e.g. where it coincides with Lawvere theories with arities, e.g. finitary monads on presheaves over inverse categories) you may well be able to, but I personally think it's likely that full dependency (e.g. at the term level) has structure that may well not be capturable by these concepts
Nathanael Arkor (Apr 07 2020 at 11:31):I also think C-systems are not a particularly natural description of dependent syntax, but, for now, that's the best analogue we have
Nathanael Arkor (Apr 07 2020 at 11:32):So I think there should be (at least) one other column, in which to put a presentation of operations with many inputs and many outputs.
I agree: if you were making a comprehensive table, then you'd also want to include sequent calculi as well as type theories :+1:
Nathanael Arkor (Apr 07 2020 at 11:34):Secondly, I believe there should be two more columns for the colored such stuff
yes, really I think we ought not to bother with the single-sorted case and just talk about "multicategories" rather than (coloured) operads
Thibaut Benjamin (Apr 07 2020 at 12:34):The single-sorted cases are pretty nice, because you are happy to end up in known territory. Lawvere theories, and operads are quite famous examples. Also the single-sorted cases connect more directly with the logical aspect of it : monoids, groups, abelian groups... all are single-sorted theories. I think that's why the single-sorted case is so much cited. But it's also "nothing special" and maybe focusing too much of it hides a bit what's really going on. Along the same lines, I remember really understanding the tensor product of vector spaces only when I realised that it was a special case of a tensor product on bimodules!
Nathanael Arkor (Apr 07 2020 at 12:43):monoids, groups, abelian groups... all are single-sorted theories
actions, modules, vector spaces, etc. are all 2-sorted theories — there are many examples of -sorted theories for any
Nathanael Arkor (Apr 07 2020 at 12:44):however, the constructions on single-sorted algebraic theories are different to the constructions on multisorted algebraic theories and tend to be much less natural from a syntactic point of view
Nathanael Arkor (Apr 07 2020 at 12:44):multisorted Lawvere theories and multicategories are also well-known territory
Nathanael Arkor (Apr 07 2020 at 12:45):so I would argue that the focus on the single-sorted setting has been primarily for historical reasons
Thibaut Benjamin (Apr 07 2020 at 13:18):There's definitely a argument for it. But in any case, let's agree on the fact that we should always keep an emphasis on multi-sorted/coloured things