Rooted Non-planar trees, Operads, and Dendroidal Sets

Stream: mathlib4

[Alvaro Belmonte]

Hello everyone,

I am interested in formalizing the theory of dendroidal sets by Moerdijk and Weiss. Before this I would like to hear if anybody has been working on formalizing the category of rooted non-planar trees and/or Operads/Multicategories. If not, i am open for suggestions or starting tips and collaborations are open for everyone.

thanks for the attention

[Alex Meiburg]

I have a definition of Operads and Symmetric Operads in #20051 . They are primarily defined to show how they fit together with Clones. (The end goal is to prove Post's Lattice.) I am not really an expert on all the things people do with operads, though, so I would welcome some feedback. In particular, is the current definition reasonable and functional for other things people would want to prove about them.

I am aware that there are several possible definitions of operads, which is why I'd like some feedback. :)

[Johan Commelin]

Very cool! Looking forward to getting the basics of operads in mathlib!