A clean understanding of universal algebra is given by the notion of cartesian operad. From it one can easily derive other approaches via Lawvere theories or finitary monads. One way or another these all identify the same collection of n-ary operations in the traditional sense. A theory which derives from some weaker notion of operad depends on operation whose arity should be thought of differently. The usual arities are in a sense redundant. The common understanding of this can be made precise with a little 2-dimansional category theory. Work on abstract syntax makes it clear that there is another subtlety in the notion of operations for an algebraic theory. Some theories have non-standard arities which are hidden in the standard presentation. This also can be made precise using ideas from higher category theory.
(Joint work with D. Petrisan) We study categories of algebras for endofunctors on Nom, the category of nominal sets in the sense of Gabbay and Pitts. We start from the fact that Nom is a full reflective subcategory of a monadic category, namely the presheaf category Set^I. We then show that the standard category theoretic proof of Birkhoff's HSP theorem can be `pushed through the adjunction' relating Nom and Set^I, thus yielding an HSP-theorem for nominal algebras. This theorem is different from the one proposed by Gabbay, and we show how to recover his theorem from ours by restricting the equational logic of universal algebra to what we call `uniform equations'. Whereas the first result is axiomatic in that it only depends on properties of the adjunction, the result on uniform equations is rather more specific to Nom and Set^I.
A $\Sigma\Pi$-category is a category obtained from another by freely adding finite products and coproducts. The theory of such categories is complicated by the presence of the units, and the fact that the free product and coproduct are not inherently distributive. Free completions with all limits and colimits were first described by Joyal. Recently, interest in the restricted setting of $\Sigma\Pi$-categories has mounted, with the presentation of a proof-theory in the form of a sequent calculus with cut-elimination by Cockett and Seely, and a polynomial decision algorithm for equality of maps by Cockett and Santocanale. In this talk I will present a notion of proof net for maps in $\Sigma\Pi$-categories. In the graphical representation the categorical equalities find a natural home as simple, strongly normalising graph-rewrites. The normal forms then provide cut-free, canonical representations of the maps in a $\Sigma\Pi$-category.
Over the past few years, we have witnessed the emergence of new and surprising connections between homotopical algebra (traditionally studied within algebraic topology) and Martin-L\"of type theory (traditionally studied within mathematical logic and theoretical computer science). The aim of the talk is to give a survey of these connections that is accessible to both pure mathematicians and theoretical computer scientists. In particular, I will describe some joint work with Richard Garner showing that categories naturally arising from Martin-L\"of type theory admit a weak factorisation system.