11
$\begingroup$

I've been looking at syntactic multicategories for mechanizing some type theory stuff.

But multicategories are pretty messy to work with in a two sorted definition like the usual dependently typed encoding.

Stating the operations alone without the laws is a mess. You need extra Forall and concat helpers too to iterate over g the list of argument Homs.

In practice you'd also add another layer of finickyness with setoids.

Class Multicategory := {
  Obj: Set ;
  Hom: list Obj -> Obj -> Set ;

  id A: Hom [A] A ;
  compose {B C}:
    Hom B C ->
    forall (g: Forall (fun o => { a & Hom A o }) B),
    Hom (concat g) C
}.

The two sorted definition as a monad in a multispan is more sensible but loses some ease of use.

I'm thinking about trying the single sorted definition or the colored operad approach.

I'd be curious if anyone has any concrete experience with mechanizing this sort of thing.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Even on paper multicategories are awful! But before going all the way to operads, I'd consider trying to represent a list of objects of length $n$ as $\mathsf{Fin}(n) \to \mathsf{Obj}$. It's isomorphic, of course, but it does make the index manipulations a bit nicer. $\endgroup$
    – Neel Krishnaswami
    Commented Mar 8, 2022 at 9:56
  • 2
    $\begingroup$ Multicategories are beautiful on paper. (-: $\endgroup$
    – Mike Shulman
    Commented Mar 8, 2022 at 16:39
  • 1
    $\begingroup$ I have an answer to this question with a full code implementation of cartesian multicategories, but the post button unfortunately does nothing. >_> $\endgroup$
    – Astra Kolomatskaia
    Commented Mar 8, 2022 at 21:55
  • 1
    $\begingroup$ Tl;DR: The definition is actually quite short and elegant! Start by reading the first 28 lines, plus the definition of derive, in the following file: github.com/FrozenWinters/stlc/blob/main/lists.agda Then continue to the main definition in lines 29-63 of this file: github.com/FrozenWinters/stlc/blob/main/contextual.agda I go on to develop the theory of weakenings and variables that is inherent to every simple contextual category. $\endgroup$
    – Astra Kolomatskaia
    Commented Mar 8, 2022 at 22:00
  • 1
    $\begingroup$ If you happen to want symmetric multicategories, I might have enough bits and pieces lying around to give a relatively quick answer. If not, I don't think the general case is actually that much harder, but I don't get to reuse some somewhat boring code. $\endgroup$
    – James Wood
    Commented Mar 11, 2022 at 21:57

1 Answer 1

Reset to default
8
$\begingroup$

[I'm posting this by proxy for Astra, who is having technical difficulties posting on this site.]

Hey! I recently completed a large scale formalisation in which I independently rediscovered cartesian multicategories as being the exactly correct and most economic way of encoding the structure of non-dependent type theory. (I refer to these as Simple Contextual Categories.) This notion is completely central to all of my constructions.

My project was to formalise Altenkirch's paper Categorical reconstruction of a reduction-free normalisation proof. The main idea is that simply typed lambda calculus is the language of cartesian closed simple contextual categories. We obtain a normalisation proof by looking at two such (CCSC) categories: presheaves and twisted glueings. I think that the main contribution of the formalisation is a particularly nice formulation of simple contextual categories, which seems to be what you're asking about. The paper on this formalisation is currently in the process of being written, but the code has been online for some time now.

In order to read the definition, first read the first 28 lines, plus the definition of derive, in the following file: https://github.com/FrozenWinters/stlc/blob/main/lists.agda

Subsequently, you can go directly to the definition of a simple contextual category in this file: https://github.com/FrozenWinters/stlc/blob/main/contextual.agda

The main definition is in lines 28-63 of the second file, and we then go on to develop the theory of weakenings and variables that is inherent to every simple contextual category.

The bulk of the project consists of constructing examples of such structures.

I believe that there is a dependent analogue of this construction; this is a current research question on which some progress has been made.

Improve this answer
$\endgroup$
7
  • $\begingroup$ I'm interested in substructural logic (specifically the closed monoidal Rel category of relationships) but I'm sure this will be helpful. $\endgroup$
    – Ms. Molly Stewart-Gallus
    Commented Mar 10, 2022 at 0:56
  • $\begingroup$ Oh, this is great! I've never even tried multicategories in Agda, because I assumed it would be an even more horrible experience than on paper. So it's genuinely surprising that this development is as clean and pretty as it is. $\endgroup$
    – Neel Krishnaswami
    Commented Mar 11, 2022 at 12:33
  • $\begingroup$ @NeelKrishnaswami I thought so too, until I sat down and did 'generalized' multi-categories (i.e. indexed by arbitrary sets instead of naturals), and that was super smooth. It's now in agda-categories. $\endgroup$
    – Jacques Carette
    Commented Mar 16, 2022 at 13:09
  • 1
    $\begingroup$ Multicategories indexed by arbitrary finite sets are sometimes called "fat" symmetric multicategories. Usually "generalized multicategories" refers to something much more general, e.g. parametrized by a monad. $\endgroup$
    – Mike Shulman
    Commented Mar 16, 2022 at 15:17
  • $\begingroup$ @JacquesCarette Score one for intrinsic scoping over De Bruijn indices, I guess! $\endgroup$
    – Mike Shulman
    Commented Mar 16, 2022 at 17:44

Not the answer you're looking for? Browse other questions tagged or ask your own question.