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: Categorical treatment of parametrized theories?

Jacques Carette (Dec 02 2022 at 09:04):

What I'm looking for is a setting for doing meta-theory that is able to talk about parametrized theories.

To be concrete: in universal algebra, one of the early constructions is that of homomorphism (between first-order, single-sorted equational theories). The "problem" is that homomorphisms, as theories, are not "in" that same setup. In particular, the best way to phrase that a particular tuple of data is a homomorphism of X structures (think X = Monoid for concreteness) involves taking in 2 Xs as 'parameters', and then specifying new data in terms of those parameters.

We know Lawvere theories are sufficient to talk about the base data of universal algebra. What's the corresponding categorical setup where one can talk about homomorphisms as data? The point is to internalize these.

Tom Hirschowitz (Dec 02 2022 at 11:58):

Not sure I'm getting the point, but taking a theory to be a locally finitely presentable category, these may all be viewed as models of some finite limit sketch, hence are all categories of functors $S \rightarrow Set$ mapping some distinguished cones to limit cones. Now a morphism in such a functor category is equivalently a functor $F\colon \mathbb{2} \rightarrow [S,Set]$ such that $F(0)$ and $F(1)$ both map distinguished cones to limit cones. By rearranging arguments, this is the same as a functor $F\colon: \mathbb{2} \times S \rightarrow Set$ preserving suitable distinguished cones in $\mathbb{2} \times S$. Morphisms thus appear to be models of a finite limit sketch, hence to form a locally finitely presentable category.

Nathanael Arkor (Dec 02 2022 at 12:14):

@Jacques Carette: If you take two monoids $M_1$ and $M_2$, then there is a set of homomorphisms $\mathrm{Mon}(M_1, M_2)$. However, for the homomorphisms $M_1 \to M_2$ to be the models of some theory, you presumably expect the models to form at least a category. What do you expect the morphisms in $\mathrm{Mon}(M_1, M_2)$ to be?

Nathanael Arkor (Dec 02 2022 at 12:22):

Another question, which might help better explain the motivation: algebraic theories are categorical representations of syntactic presentations of universal algebras. Is there a corresponding syntactic presentation of homomorphism you want to capture categorically? If not, your question seems perhaps better placed as an universal algebraic / type theoretic question rather than a categorical one (since theories are conceptually motivated by syntax).

Jacques Carette (Dec 02 2022 at 12:22):

@Nathanael Arkor I expect the objects to be triples, with the first being a function from the carrier of $M_1$ to the carrier of $M_2$, and the next two would be commutative squares expressing preservation of unit and the binary operation. The morphisms are then homotopies of the underlying function (likely with an additional commutation condition).

Nathanael Arkor (Dec 02 2022 at 12:23):

commutative squares expressing preservation of unit and the binary operation

This is a property of the first piece of data, not data itself, no?

Nathanael Arkor (Dec 02 2022 at 12:24):

Maybe I misunderstand what you mean.

Jacques Carette (Dec 02 2022 at 12:26):

For the second question: absolutely, that's the whole motivation! I'm writing down all sorts of "records" in Agda that represent things like Homomorphism and lots of other information associated to usual constructions in universal algebra. Syntactically, these sure look like theories too - but of a slightly different kind.

Type-theoretically, I have not seen that much about "parametrized records". So I was hoping that this had been figured out categorically already.

Jacques Carette (Dec 02 2022 at 12:28):

Nathanael Arkor said:

commutative squares expressing preservation of unit and the binary operation

This is a property of the first piece of data, not data itself, no?

Correct. But from the point of view of proof-relevant type theory, they are often treated as data (and they are in agda-categories).

Jacques Carette (Dec 02 2022 at 12:28):

@Tom Hirschowitz My knowledge of finite limit sketches is thin, so it's going to take me some time to unpack that - but thanks for the lead.

Nathanael Arkor (Dec 02 2022 at 12:29):

What's the definition of a homotopy between monoid homomorphisms?

Tom Hirschowitz (Dec 02 2022 at 12:34):

Probably, there is some higher-level understanding of this, along the lines of:

• locally finitely presentable (lfp) categories are closed under some weighted limits in CAT;

• $[\mathbb{2},\mathcal{C}]$ is the limit of $\mathcal{C}$ weighted by $\mathbb{2}$;

• therefore lfp categories are closed under "taking morphisms".

But I'm not confident enough to be sure without digging a bit more.

Btw, did you really mean the theory of morphisms to be the arrow category?

Tom Hirschowitz (Dec 02 2022 at 12:36):

(Related to Nathanael's questions...)

Nathanael Arkor (Dec 02 2022 at 12:40):

(I think it's possible to define some categories whose objects are homomorphisms between two models of an algebraic theory, but much less obvious that any of them are useful to consider, from an algebraic/type theoretic point of view. So I think one really needs to proceed from the syntax to the category theory, rather than the other way around. I'm not aware of any categorical theory that sounds like what Jacques is after, which suggests to me the syntactic theory needs to be worked out first.)

Nathanael Arkor (Dec 02 2022 at 12:41):

In other words, I think that the answer to this question:

So I was hoping that this had been figured out categorically already

is "it has not".

Nathanael Arkor (Dec 02 2022 at 12:42):

That said, if there is a precise treatment from the syntactic point of view, then it may be that the categorical interpretation follows quickly therefrom.

Jacques Carette (Dec 02 2022 at 13:23):

Nathanael Arkor said:

What's the definition of a homotopy between monoid homomorphisms?

I meant homotopy of the underlying function on the carriers, sorry I was not sufficiently precise there.

The upshot still seems to be: figure out the type-theoretic version of this first. The 'syntactic' part is straightforward, and was worked out in Yasmine Sharoda's PhD Thesis. This amounts to the 'formalization' of the fact that most constructions from universal algebra can be seen as (generalized) folds over their presentations.

My intuition is that such folds usually have a nice categorical explanation. Here I'm stuck on even naming the categories involved, never mind the meta-theory in which the Functor lives!

Damiano Mazza (Dec 02 2022 at 14:25):

Jacques Carette said:

To be concrete: in universal algebra, one of the early constructions is that of homomorphism (between first-order, single-sorted equational theories). The "problem" is that homomorphisms, as theories, are not "in" that same setup.

What do you mean that it is not in the same setup? That the theory of homomorphisms of a Lawvere theory is not itself a Lawvere theory? That's only the case if you absolutely want Lawvere theories to be single-sorted. If you allow algebraic theories to have arbitrarily many sorts, then for every algebraic theory $\mathbb T$ there is an algebraic theory $\mathbb H\mathrm{om}_{\mathbb T}$ whose models are exactly triples $(M,f,N)$ where $M$ and $N$ are models of $\mathbb T$ and $f$ is a homomorphism $M\to N$. $\mathbb H\mathrm{om}_{\mathbb T}$ will have twice as many sorts as $\mathbb T$ (each sort has two copies). In particular, if $\mathbb T$ is single-sorted, then $\mathbb H\mathrm{om}_{\mathbb T}$ will have two sorts, but it will still be algebraic (I mean, just an equational theory).

For example, the theory of monoid homomorphisms has two sorts $M_1,M_2$, two binary function symbols $m_1:M_1^2\to M_1$ and $m_2:M_2^2\to M_2$, two constants $e_1:M_1$ and $e_2:M_2$, and an extra function symbol $h:M_1\to M_2$. Its axioms are the monoid axioms for $m_1,e_1$ and $m_2,e_2$, plus the axioms $h(m_1(x,y))=m_2(h(x),h(y))$ and $h(e_1)=e_2$. It is true that the two sorts $M_1,M_2$ are "parameters" of some kind, but it's just like the single sort of the theory of monoids is a "parameter" for choosing a set. I don't see why you would need any special "parametrization". But I suspect that I am misunderstanding what you mean...

(By the way, what I said is just a syntactic reformulation of what @Tom Hirschowitz said in his first comment).

Damiano Mazza (Dec 02 2022 at 14:30):

Ah, maybe now I understand: your problem is that the above setup doesn't give you the notion of morphism between homomorphisms that you are looking for? Is this the notion of "homotopy" you are talking about? (Which is still unclear to me, sorry).

Damiano Mazza (Dec 02 2022 at 14:33):

Just to be clear: in the above setup, a morphism from a monoid homomorphism $h:M_1\to M_2$ to a monoid homomorphism $h':M_1'\to M_2'$ is just a pair of monoid homomorphisms $f_1:M_1\to M_1'$, $f_2:M_2\to M_2'$ making the obvious square commute.

Damiano Mazza (Dec 02 2022 at 14:34):

So the resulting category is indeed the arrow category of $\mathbf{Mon}$, as mentioned above.

Morgan Rogers (he/him) (Dec 02 2022 at 14:56):

I think the arrow category is probably what @Jacques Carette is looking for, since the implication of asking for homotopies is that this theory is being interpreted in a $(2 \text{(or more)},1)$-category where the commutative square defining a morphism of models of the theory will be interpreted as an invertible $2$-cell filling the square in the semantics.

Jacques Carette (Dec 02 2022 at 15:27):

@Damiano Mazza So the reason I want 'parametrized' is that I really don't want 2 copies of the theory of monoids to be embedded in the theory of homomorphisms. [I'm completely fine with going multi-sorted from the start.] Otherwise, yes, if you "inline" everything, then one doesn't need to go beyond algebraic theories for homomorphism. Also, I'm really interested in theory (presentations), I think the story at the level of models is simpler.

My motivation comes as an implementor of systems for doing mathematics, and thus I am inexorably stuck in syntax, or at least must look at many things from the side of syntax.

I was rather expecting to have to use bicategories / fibrations / double categories as a setting to be able to say what I want.

Morgan Rogers (he/him) (Dec 02 2022 at 15:32):

Jacques Carette said:

Damiano Mazza So the reason I want 'parametrized' is that I really don't want 2 copies of the theory of monoids to be embedded in the theory of homomorphisms. [I'm completely fine with going multi-sorted from the start.]

Could you explain what you mean? As was mentioned earlier by @Tom Hirschowitz , you can take a weighted limit in a 2-category of syntactic categories to get the theory $[2,\mathcal{C}]$, but cashing it out syntactically you necessarily get two copies of the original theory back out. What exactly are you hoping to avoid here?

Jacques Carette (Dec 02 2022 at 15:51):

I'm trying to find a theoretical framework that would let me explain

record MonoidHomomorphism(M N : Monoid) : Set _ where
  private
    module M = Monoid M
    module N = Monoid N
  field
    hom : M.Carrier -> N.Carrier
    pres-e : hom (M.e) = N.e
    pres-* : (x y : M.Carrier) -> (hom x) N.* (hom y) = hom (x M.* y)

(forget the the "private module" bits as far as the meta-theoretical explanation goes, that's just convenience).

The above is actually something we can generate, given any presentation of a theory (here, I used Monoid). But the above is itself a 'theory', but in a slightly different setting.

Yes, everything in the presentation of Monoid has to be available and visible, but it is not in the theory above, which has just 3 components. There is a 'phase separation' between Monoid and MonoidHomomorphism that I would like to preserve.

Morgan Rogers (he/him) (Dec 02 2022 at 15:56):

Hmm it seems to me that this construction is not the theory of monoid homomorphisms, it's the construction, given $M$ and $N$, of the set of monoid homomorphisms from $M$ to $N$. It's a "comma theory", rather than an "arrow theory".

Morgan Rogers (he/him) (Dec 02 2022 at 15:58):

(I can try to be more detailed if you need)

Jacques Carette (Dec 02 2022 at 16:00):

Why comma rather than fibration? I was expecting things (like Isomorphism and many other similar constructions) to somehow be 'above' the theory Monoid. [But I'm clearly navigating waters I'm unfamiliar with, so my expectations could be completely wrong.]

Jacques Carette (Dec 02 2022 at 16:03):

But: I do agree that this specifies the set of monoid homomorphisms from $M$ to $N$. Yet I don't see this as fundamentally different than the record (with 0 parameters) that specifies Monoid itself.

Jacques Carette (Dec 02 2022 at 16:08):

I now understand the point of departure: I have very deeply internalized dependent type theory, and forget that others have not. So to me there is no such thing as a $\mathsf{Hom}$ set for a category, there is only a parametric family $\mathsf{Hom(A,B)}$ of Hom sets, one per pair of objects. The other thing isn't something to ever consider.

Similarly for Homomorphism. It's a family.

Morgan Rogers (he/him) (Dec 02 2022 at 16:09):

The answer to "why comma" is this diagram. On the outside you have a square where the lower composite functor corresponds to $M$, the upper composite functor corresponds to $N$, and the natural transformation between these is the monoid homomorphism. This factors through a comma construction (it's a weighted colimit rather than a weighted limit), which is the syntactic category for the theory of homomorphisms from $M$ to $N$.

Morgan Rogers (he/him) (Dec 02 2022 at 16:15):

But having drawn it, it seems that there could be more models of that comma theory than the ones I intended, because there could be more interesting functors from the comma to $\mathrm{Set}$ (in contrast to a comparable classifying topos situation I am more familiar with). So don't feel too constrained by the preceding message.

Mike Shulman (Dec 02 2022 at 16:15):

Jacques Carette said:

But: I do agree that this specifies the set of monoid homomorphisms from $M$ to $N$. Yet I don't see this as fundamentally different than the record (with 0 parameters) that specifies Monoid itself.

From a record point of view, it's not. But not every record type is an algebraic theory.

Mike Shulman (Dec 02 2022 at 16:15):

Nor does every record type even specify the objects of some category.

Mike Shulman (Dec 02 2022 at 16:20):

For fixed $M,N$, there is an (infinitary) first-order theory that describes the notion of "monoid homomorphism from $M$ to $N$". In fact, it is a "propositional" theory, with zero sorts, because such monoid homomorphisms (for fixed $M,N$) form a set rather than a category. It consists of:

• For each $m\in M$ and $n\in N$, an atomic proposition $\phi(m,n)$
• For each $m\in M$, an axiom $\bigvee_{n\in N} \phi(m,n)$
• For each $m\in M$ and $n_1,n_2\in N$ with $n_1\neq n_2$, an axiom $\neg (\phi(m,n_1) \wedge \phi(m,n_2))$
• An axiom $\phi(e_M, e_N)$
• For each $m_1,m_2\in M$ and $n_1,n_2\in N$, an axiom $\phi(m_1,n_1) \wedge \phi(m_2,n_2) \to \phi(m_1m_2,n_1,n_2)$

Mike Shulman (Dec 02 2022 at 16:25):

In general, you're right that categorically when talking about parametrized things you want to talk about fibration-like things, where $p:D\to C$ means that the objects of $D$ are "parametrized" by those of $C$. The arrow category that others have mentioned comes with a projection to two copies of the base category, $C^{\to} \to C\times C$, which categorically exhibits this parametrized nature of homsets. However, this projection is neither a fibration nor an opfibration, nor are its fibers very well-behaved categorically: they are discrete sets, not (e.g.) algebraic or even locally presentable categories. So if you want to consider it as the models of some kind of "parametrized theory" over $C\times C$, the notion of "theory" will have to be extremely general, such as the infinitary first-order one I gave.

Jacques Carette (Dec 02 2022 at 16:29):

Mike Shulman said:

From a record point of view, it's not. But not every record type is an algebraic theory.

Nor does every record type even specify the objects of some category.

Completely agree with that! I am specifically interested in those record-type-definitions that are a presentation of an algebraic theory, and a reasonable way to talk about the corresponding record that encodes 'homomorphism'. It certainly should be some kind of 'theory', but it doesn't necessarily be an object of a category.

Jacques Carette (Dec 02 2022 at 16:31):

I don't understand your first-order theory: how is $\phi$ supposed to encode $\textsf{hom}$ ?

Jacques Carette (Dec 02 2022 at 16:35):

I'm willing to consider quite general theories (like Cartmell's generalized algebraic theories) as a setting. I would much prefer that over going 'infinitary'. At the end of the day, I want to say things inside MLTT. My eventual goal is indeed to mechanize the concept of 'homomorphisms' (and 20+ other constructions) for such GATs.

Reid Barton (Dec 02 2022 at 16:40):

If an algebraic theory means a GAT, i.e. some kind of telescope of type/term/equation formation rules, then a theory parameterized by some other theory T ought to be a telescope that starts from the context of the theory T.

Reid Barton (Dec 02 2022 at 16:40):

The whole telescope will have models that form a locally presentable category, which will have a forgetful functor to the models of T, which may or may not be fibered in an interesting way.

Jacques Carette (Dec 02 2022 at 16:55):

@Reid Barton That was my intuition as well. Intuition is a far cry from a proper explanation. I was hoping that this had been done fairly generally.

I've actually done some of this jointly with Russell O'Connor, though it's really just a rephrasing of materials in Bart Jacobs' book. I just can't help thinking that there ought to be a simple way to approach this problem.

Nathanael Arkor (Dec 02 2022 at 17:08):

You can certainly parameterise a theory by another (taking coslices in the category of GATs), but this seems far more general than warrants the name "homomorphism".

Nathanael Arkor (Dec 02 2022 at 17:08):

But if this is actually what you were looking for, then there is a clean categorical treatment.

Reid Barton (Dec 02 2022 at 17:11):

I was assuming that "homomorphisms of Ts" was an example--maybe a special one in that you can automatically derive the (relative) GAT for homomorphisms-of-Ts from the one for Ts, but not the only kind of example.

Jacques Carette (Dec 02 2022 at 17:13):

@Reid Barton Correct, it is but one example of a construction from theory presentations to presentations of T-parametrized things. It's easy to enumerated 20+ such constructions in common use.

Nathanael Arkor (Dec 02 2022 at 17:17):

Oh, I think we all mistakenly focused on the homomorphism example. Do coslices achieve what you are after, then? If $T$ is a theory, the category of coslices $T/\mathrm{GAT}$ comprises those theories defined in the context of the operations and equations of $T$. For a homomorphism, where we want to parameterise by two theories $T$ and $T'$, we may first take the coproduct $T + T'$ and then coslice under this theory.

Reid Barton (Dec 02 2022 at 17:30):

Ah so it's unclear to me at what level we are talking about parameterization. For example, is the theory of "modules over a ring R" parameterized by the ring R or by the theory "rings".

Jacques Carette (Dec 02 2022 at 17:30):

It may well be that the category of coslices is what I'm after. There must be some 'op' thing going on, as I was expecting to consider $T \times T'$ . The telescope view that @Reid Barton mentions was the picture I had in mind.

Jacques Carette (Dec 02 2022 at 17:34):

@Reid Barton I'm thinking of a presentation of the theory of $R$-modules as parametrized over the presentation of the theory of rings. Any given instance will necessitate a fixed ring $R$, but it can also remain abstract for certain purposes (i.e. a promise of a ring later rather than an actual ring now.) To me that coincides with the "take a context and split it into two parts, the first bit that specifies a ring, and the next bit that uses the first bit, that specifies module".

Jacques Carette (Dec 02 2022 at 17:36):

The 'homomorphism' example has one copy of the monoid Monoid in the context, two promises of things of that type, and then the bits that say what a homomorphism is.

Nathanael Arkor (Dec 02 2022 at 17:50):

Jacques Carette said:

It may well be that the category of coslices is what I'm after. There must be some 'op' thing going on, as I was expecting to consider $T \times T'$ . The telescope view that Reid Barton mentions was the picture I had in mind.

I think the opposite comes in via the fact that $\mathrm{Mod}(T + T') \cong \mathrm{Mod}(T) \times \mathrm{Mod}(T')$, so you take products of the categories of models, but coproducts of the theories.

Nathanael Arkor (Dec 02 2022 at 17:52):

Jacques Carette said:

Reid Barton I'm thinking of a presentation of the theory of $R$-modules as parametrized over the presentation of the theory of rings. Any given instance will necessitate a fixed ring $R$, but it can also remain abstract for certain purposes (i.e. a promise of a ring later rather than an actual ring now.) To me that coincides with the "take a context and split it into two parts, the first bit that specifies a ring, and the next bit that uses the first bit, that specifies module".

Using coslices, you can consider either as appropriate. Every model $M$ of a theory $T$ (e.g. a specific ring) induces a theory $T_M$ (the "structure" associated to the model in the terminology of Lawvere), and so you can consider parameterisation either by $T$ or by $T_M$.

Jacques Carette (Dec 02 2022 at 17:57):

That sounds great @Nathanael Arkor . Where can I read more about this?

Nathanael Arkor (Dec 02 2022 at 18:40):

There was a recent draft by Cartmell that discussed some of these topics if I remember it correctly. It's been a while since I looked at it, though, so I don't remember how much detail he went into.

Mike Shulman (Dec 02 2022 at 20:14):

Jacques Carette said:

I don't understand your first-order theory: how is $\phi$ supposed to encode $\textsf{hom}$ ?

$\phi(m,n)$ is the assertion that the homomorphism maps $m$ to $n$.

Mike Shulman (Dec 02 2022 at 20:15):

A model of the theory assigns a truth value to each atomic proposition $\phi(m,n)$, and the axioms ensure that these truth values precisely encode a function which is a homomorphism.

Mike Shulman (Dec 02 2022 at 20:18):

I'm a little confused because you said you don't want two copies of the theory of rings to be embedded in the parametrized theory of homomorphisms, but isn't that precisely what the coslice approach does?

Mike Shulman (Dec 02 2022 at 20:19):

If $T$ is the theory of rings, then your theory of homomorphisms as a telescope is $T, T, \hom_T$, with the inclusion from $T,T$ doing the embedding and making it an object of the coslice under $T,T$.

Jacques Carette (Dec 03 2022 at 11:58):

So I see my telescope as

$T : *; T = {Carrier : *; ...}\ ||\ M : T, N : T\ |\ \mathsf{Hom}_{T} : *; \mathsf{Hom}_{T} = {...}$,

where $\ ||\$ and $\ |\$ are like $\ , \$ but insert a 'barrier', and $T = {...}$ is a presentation of a theory, and I use ; to couple together a type assertion with a definition.

The point is that ${Carrier : *; ...}$ only occurs once, not twice. (This matters for scaling.) Defining what $T$ means is quite different from assuming having two instance $M, N$ that satisfy this interface.

Mike Shulman (Dec 03 2022 at 22:27):

I can't even parse that. Can you add some parentheses?

Mike Shulman (Dec 03 2022 at 22:27):

What is a "barrier"?

Mike Shulman (Dec 03 2022 at 22:32):

But if I understand correctly what you're getting at, you still do have two copies of $T$, namely $M$ and $N$. The fact that you don't have to write out the definition of $T$ twice syntactically is irrelevant from a categorical perspective; the data is still there.

Jacques Carette (Dec 05 2022 at 15:30):

Let's forget the context and barriers for now, your last paragraph is where things are interesting:

But if I understand correctly what you're getting at, you still do have two copies of TT, namely MM and NN. The fact that you don't have to write out the definition of TT twice syntactically is irrelevant from a categorical perspective; the data is still there.

For scaling of a comfortable development environment, not having the definition syntactically twice is extremely important, and definitely part of my question! [Some of the 'solutions' at the start of this thread would basically mean doing exactly that.] If I'm trying to formalize category theory in type theory, lots of gadgets become extremely cumbersome if I have to repeat everything. That's not how category theory is actually done either.

Yes, absolutely, the data is still there, that's the whole point of having $M$ and $N$ as parameters. It's there in a short and abstract way.

Tom Hirschowitz (Dec 05 2022 at 15:49):

But wait, if you first define, say the sketch for your theory, and then take the product with 2, you only need to write it down once, right? Similarly, if you first define the lfp of monoids and then take some suitable weighted limit, you only wrote it down once. I'm still not sure I get your goal right, so sorry if this is off the point.

Jacques Carette (Dec 05 2022 at 15:58):

@Tom Hirschowitz Sketches are an interesting lead, as they are some kind of categorical presentation of theories. I haven't had the time yet to pursue that seriously. [What I really want to do first is to formalize sketches into agda-categories, that ought to really force me to learn much of the details.]

Mike Shulman (Dec 05 2022 at 18:47):

My point is that you were asking about a categorical setup, and category theory doesn't notice fine distinctions like that, as important as they may be for implementation.

Jacques Carette (Dec 05 2022 at 19:55):

@Mike Shulman Thanks, that does help. And it even makes sense, now that I've been forced to really lay out what I was trying to puzzle out.

Tom Hirschowitz (Dec 06 2022 at 06:13):

@Jacques Carette Beware that sketch theory relies heavily on ordinals. I'm curious about which approach to them you'll adopt!

Jacques Carette (Dec 06 2022 at 10:41):

I'm also curious to see which one will end up 'working' in my setting (aka as close to MLTT with universes as possible)! I think I want to complete the work on multicategories and on double categories first, as I think resolving the technical difficulties there will have an influence on that.

Right now, my version of multicategories is type-indexed instead of $\mathbb{N}$-indexed, and double categories are done 'over equations' instead of assuming strictness. That appears to work out fine, but I need to push through more bits of the theory to make sure it really does.