Define multicategories

[anshwad10]

This is a generalization of a multicategory like https://gist.github.com/plt-amy/174cf949e4cad7a24c1c73d0cdc6c35b However, I didn't require isArity to be a proposition so that the finite ordinals also qualify as arities. This is a generalization of both non-symmetric and symmetric multicategories, and it also allows multicategories with infinite-arity morphisms. I am currently not sure of the relation to Tom Leinster's generalized multicategories.

[anshwad10]

I'll add more when the next version of cubical is supported and the error is fixed

[anshwad10]

I am currently not sure of the relation to Tom Leinster's generalized multicategories.

I think Tom Leinster's multicategories are actually more general than these: Given some S : ArityType there is a (wild) monad M on Type defined by M X = Σ[ I ∈ Arity ] ⟨ I ⟩ → X; isArity-⊤ provides the unit, isArity-Σ gives the join, and isArity-idl isArity-idr isArity-assoc give the monad laws. An S-multicategory in this sense is precisely a M-multicategory in their sense
So I'm going to try again with a more general definition parameterized by an arbritrary wild monad

[anshwad10]

Interestingly, this seems to be a similar approach as https://github.com/hmoeneclaey/operads/blob/master/Operad.agda
Funny how both of them seemed to have come up with similar ideas independently

[mortberg]

Interestingly, this seems to be a similar approach as https://github.com/hmoeneclaey/operads/blob/master/Operad.agda Funny how both of them seemed to have come up with similar ideas independently

Could you please add this reference in a comment in the code? That way it won't get lost

[anshwad10]

Could you please add this reference in a comment in the code?

What code are you referring to? This pull request is closed, and though I intend to make another PR formalizing multicategories sometime in the future, I'm going to use a different approach (based on the wild monads #1265), so it won't really be relevent if i put it there

[mortberg]

Oh, I did not see that the PR was closed. I just thought that it would be better to have a pointer to https://github.com/hmoeneclaey/operads/blob/master/Operad.agda in the code instead of on Github as that will make it better documented in the code base for the future