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: learning: questions

Topic: Generalization of operads

Asad Saeeduddin (Jun 06 2020 at 09:16):

Is it possible to substitute the natural numbers that occur in the definition of (non-symmetric, symmetric, colored) operads with some other monoid?

Pastel Raschke (Jun 06 2020 at 12:17):

i believe that would fall under generalized multicategories

Pastel Raschke (Jun 06 2020 at 12:20):

Multicategories are monads in a bicategory of spans of shape X←R→Y* where Y* is the set of finite lists of elements of Y. In order to compose spans of this type, one uses the fact that (−)* has itself the structure of a monad on Set, namely the list monad or “free monoid” monad. The idea of a generalized multicategory is to replace this monad by some more general monad T.

Asad Saeeduddin (Jun 06 2020 at 12:37):

agghhhhhh, i was so proud of myself for working out this monad idea

Asad Saeeduddin (Jun 06 2020 at 12:37):

i was doing this in Agda just now:

record Monad (m : Set ℓ → Set ℓ) : Set (suc ℓ)
  where
  field
    {{functor}} : Functor m
    pure : ∀ {a} → a → m a
    join : ∀ {a} → m (m a) → m a
    liftA2 : ∀ {a b c} → (a → b → c) → m a → m b → m c

open Monad {{...}}

record Singleton (m : Set (suc ℓ) → Set (suc ℓ)) : Set (suc ℓ)
  where
  field
    sfunctor : m (Set ℓ) → Set ℓ

open Singleton {{...}}

record MultiCategory {m : Set (suc ℓ) → Set (suc ℓ)} (_⇒ₘ_ : m (Set ℓ) → Set ℓ → Set ℓ) : Set (suc (suc ℓ))
  where
  field
    {{mm}} : Monad m
    {{sm}} : Singleton m
    idₘ : ∀ {a} → pure a ⇒ₘ a
    _∘ₘ_ : ∀ {as} {bs} {c} → bs ⇒ₘ c → sfunctor (liftA2 {{mm}} _⇒ₘ_ as bs) → join as ⇒ₘ c

Asad Saeeduddin (Jun 06 2020 at 12:37):

having started with lists for colored operads

Peter Arndt (Jun 06 2020 at 12:40):

I see no reason not to be proud...

Asad Saeeduddin (Jun 06 2020 at 12:42):

I just meant that I thought it was an original idea, but I've had this experience with ncatlab enough times that I should have known better

Jacques Carette (Jun 06 2020 at 12:45):

@Asad Saeeduddin You should seriously consider contribution to agda-categories ! Right now, that library has an odd definition of 'Indexed Multicategory' only (https://github.com/agda/agda-categories/blob/master/src/Categories/Multi/Category/Indexed.agda), which was more 'natural' from a type-theoretic point of view.

Of course, we'll want laws, not just Haskell-style lawless definitions... And writing down the laws is where all the hard stuff comes in. The usual laws surreptitiously involve using a huge number of theorems as invisible rewrites.

Asad Saeeduddin (Jun 06 2020 at 12:47):

thanks for the pointer. I'm sure there's already law-equipped definitions of functor, monad etc. somewhere in the standard library that I should be relying on, I'll try to thread the evidence from those into it once I get up to at least one instance (probably multifunctions)

Jacques Carette (Jun 06 2020 at 12:49):

We're very open to all sorts of contributions - nothing too small. Last one I merged in was someone fixing a typo in a comment! Any part of category theory we haven't done yet, we're happy to look at. Also, some parts we have done can be critiqued-then-improved.

James Wood (Jun 06 2020 at 13:13):

Asad Saeeduddin said:

I'm sure there's already law-equipped definitions of functor, monad etc. somewhere in the standard library

I don't think there are, but I'm sure there are in agda-categories.