Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: dependent operads

Nathanael Arkor (Mar 25 2020 at 15:40):

@Chaitanya Leena Subramaniam: let's continue the conversation here, so as not to interrupt the introductions thread

Nathanael Arkor (Mar 25 2020 at 15:41):

that actually answers one of the questions I had — I was wondering what the relationship to the Second-Order and Dependently-Sorted Abstract Syntax paper was, because this is the one other place I've seen a notion of "dependent multicategory" be defined

Nathanael Arkor (Mar 25 2020 at 15:41):

it's much clearer now that you've pointed that out, thank you!

Nathanael Arkor (Mar 25 2020 at 15:42):

this is interesting, because one of the issues I had with using finitary monads on a presheaf category is that in some sense, it's not "big enough"

Nathanael Arkor (Mar 25 2020 at 15:43):

that is, if you start with the Lawvere theory–finitary monad correspondence, but allow sorting by an arbitrary category, taking identity-on-objects functors from the free finite limit completion of the category is too restrictive

Nathanael Arkor (Mar 25 2020 at 15:43):

because you don't get all the limits with the morphisms in the codomain

Nathanael Arkor (Mar 25 2020 at 15:44):

that is, identity-on-objects functors are only really good enough for limits of discrete diagrams, like products

Nathanael Arkor (Mar 25 2020 at 15:45):

I hadn't realised that finitary monads on presheaf categories coincided with Marcelo's notion of $\Sigma_0$-model with substitution, but that makes perfect sense now

Nathanael Arkor (Mar 25 2020 at 15:46):

because the $\Sigma_0$-model is like a "dependent type theory without operators"

Nathanael Arkor (Mar 25 2020 at 15:47):

and it's the lack of operators that's characteristic about category-sorted Lawvere theories, or finitary monads on presheaf categories

Nathanael Arkor (Mar 25 2020 at 15:50):

if I recall correctly, the notion of $\Sigma_n$-model with substitution wasn't quite satisfactory, because the substitution wasn't quite expressive enough..? I'd have to think about it a bit more to remind myself

Nathanael Arkor (Mar 25 2020 at 15:52):

have you been reformulating the $\Sigma_n$-models in your framework, or are you approaching it differently, if you don't mind me asking?

Chaitanya Leena Subramaniam (Mar 25 2020 at 15:52):

Could you explain what you mean when you say that id-on-objects functors are not enough?
Identity-on-objects functors that are "Lawvere theories with arities" for the arity functor $Fin(C) \hookrightarrow \widehat C$ in the sense of (Berger, Melliès, Weber) correspond precisely to the finitary monads on $\widehat C$ (this is an equivalence of categories). That is every finitary monad corresponds to an essentially unique id-on-objects functor from $Fin(C)$.
(Here $Fin(C)$ is the finite-colimit completion of $C$, so $Fin(C)^{op}$ is the finite limit completion of $C^{op}$.)

Chaitanya Leena Subramaniam (Mar 25 2020 at 15:55):

$\Sigma_n$-models are kinda tricky. Syntactically, I think they correspond to type signatures that are defined inductive-inductively --- sometimes these are called "quotient inductive inductive types", and these are certainly strictly more than the finitary monads on $\widehat C$. I haven't yet started thinking about them properly, I'm afraid to say.

Nathanael Arkor (Mar 25 2020 at 15:59):

I mean something like this:
the intuition behind a Lawvere theory is that you fix a set of sorts $S$, and then you're interested in algebraic structures whose operators are $S$-sorted — the operators and equations themselves are unrestricted
a Lawvere theory captures this with an identity-on-objects functor from the free cartesian category on $S$ — here, the objects of the codomain are exactly the contexts of algebraic operators
however, if you consider finite limits instead, then the same construction doesn't work so well — if you take an identity-on-objects functor from the free finite limit completion of a small category $\mathbb S$, the contexts of the codomain are just those that are "free" — if you have an operator $f : A \to B$, then you can't describe an operator in the context $a : A, b : B(f(a))$ — because this context is represented by a pullback along the morphism representing $f$ — and this context doesn't, in general, exist (or has to be equal to a context without it), because it doesn't exist in the free finite limit completion of $\mathbb S$

Nathanael Arkor (Mar 25 2020 at 15:59):

so I think "Lawvere theories with arities" don't satisfactorily capture dependent theories, only simple theories

Nathanael Arkor (Mar 25 2020 at 16:00):

another way of saying this is that the "finite limit version of Lawvere theory" does not correspond to "essentially algebraic theory", but you want it to

Nathanael Arkor (Mar 25 2020 at 16:02):

Syntactically, I think they correspond to type signatures that are defined inductive-inductively --- sometimes these are called "quotient inductive inductive types"

I think this is close to what they should be, yes — QIITs have essentially the same signatures as GATs, and $\Sigma_n$-models are supposed to model GATs, or something close to them

Nathanael Arkor (Mar 25 2020 at 16:03):

likewise, I'm not quite sure what the precise relationship is, though

Chaitanya Leena Subramaniam (Mar 25 2020 at 16:04):

Yep, you're describing precisely the inductive-inductive stuff I mentioned :)
Indeed simple theories don't capture all dependent theories, only those that describe finitary monads on $[\mathbb S,Set]$ for some category $\mathbb S$. In fact if you want to hope for a syntactic description (à la usual Lawvere theories), you have to restrict to an inverse $\mathbb S$. (But you already know all this, I guess).

Nathanael Arkor (Mar 25 2020 at 16:05):

inverse categories are simple categories without finite fan-out, if I understand correctly?

Nathanael Arkor (Mar 25 2020 at 16:07):

right, I think I'm on the same page: you can capture the $\Sigma_0$ notion of theory with these finitary monads (so arguably some dependent theories), but not all dependent theories (e.g. $\Sigma_n$ for $n \ge 1$)

Nathanael Arkor (Mar 25 2020 at 16:08):

it's a very interesting topic: I'll be keen to see what you come up with :)

Chaitanya Leena Subramaniam (Mar 25 2020 at 16:08):

Exactly. The finite fan out property ensures that every "tree" of dependencies of an "atomic type", i.e. an object of $\mathbb S$, is a finite tree. Which in turn means that each such object is a type in a finite context of variables. Another equivalent way to say this is that every finitely presentable presheaf is a finite cell complex.

Nathanael Arkor (Mar 25 2020 at 16:10):

I haven't looked at cell complexes before, so I shall have to do so, thanks