### Attendees and Abstracts

(Slides here)

Title: Revisiting the term calculus for BCST style proof-nets

Title: Isotropy theory, categorically

Abstract:
Given an action of a group on a set, we may consider the subgroup consisting of those elements which fix a given element; this is called the isotropy subgroup at that element. Similar ideas occur in the theory of inverse semigroups, and topological groupoids. In this tutorial, I will introduce a very general category-theoretic concept of isotropy which captures these examples. In particular, I will explain what isotropy of a small category is, and more generally what the isotropy group of a Grothendieck topos (generalized space) looks like. Time permitting, we will look at higher-order isotropy as well.

Title: Inverse sums in inverse categories

Abstract:
Restriction categories as described by Cockett and Lack provide us with an algebraic axiomatization of partiality in a category. Inverse categories are restriction categories in which each map has a partial inverse. In such a category, requiring that the category has products or co-products forces the inverse category to have a rather simple structure.

In this talk we will describe the addition of a construct called an "inverse sum". An inverse sum is intended to provide much of the richness of a co-product, without forcing the category to become trivial. We will show how the inverse sum allows us to describe disjointness of maps, disjoint joins and an inverse sum tensor. Additionally we will show how an inverse category, with an inverse sum tensor, is equivalent to a certain matrix category.

This is part of an ongoing research program to describe reversible computing categorically and link that description to categorical descriptions of standard computing.

Title: Introducing tangent categories

Abstract: This talk will give a brief introduction to two categorical structures - Cartesian differential categories and tangent categories.  Both arose out of a desire to give an axiomatic foundation for settings in which an operation resembling differentiation exists.  I'll describe the relationship between these two structures and view them both through the guiding example of the category of smooth maps between powers of R.

Title: An alternative view of the tangent category axioms

Abstract: Tangent categories, first described by Rosicky, encompass a variety of concrete settings for differential geometry.  Recent work has shown that much of the theory of differential geometry - for example, vector fields, the Lie bracket, vector bundles, and connections - can be developed in this abstract setting.  However, the axioms of a tangent category can seem quite ad-hoc.  They involve not only an endofunctor on the category (representing the tangent bundle) but a number of natural transformations with non-obvious properties.

In this talk, I'll describe an alternative viewpoint for these axioms.  I'll show how the axioms for a tangent category can be seen as intuitive refinements of a much simpler structure (a category with an endofunctor and a natural transformation to the identity).  As a consequence, I'll describe what tangent categories without addition'' would look like.

Title: Categories with representable tangent structure and models of SDG associated to codifferential categories

Abstract:
We show that every suitable codifferential category in the sense of Blute-Cockett-Seely gives rise to a category with representable tangent structure in the sense of Rosick\'y and Cockett-Cruttwell and, under an additional hypothesis, a model of synthetic differential geometry.  Given any suitable codifferential category (C,T,d), so that T is a given monad on C, we show that an associated "Weil T-algebra" W(1) serves as an infinitesimal object D (in the sense of Cockett-Cruttwell) in the opposite Aff_T := (C^T)^{op} of the category of T-algebras.  For example, when C is the category of K-modules for a commutative ring K and T is the symmetric K-algebra monad on C, W(1) is the K-algebra of dual numbers K[x]/(x^2) and Aff_T is the category of affine K-schemes. In general, letting K be the monoidal unit of C, the infinitesimal object D is a subobject of the "affine T-line" R = Spec(TK) in Aff_T and consists of square-zero elements. The object D is exponentiable in Aff_T, and the formal Kock-Lawvere axiom R x R \cong R^D holds. Under an additional hypothesis, D consists of exactly the square-zero elements of R, so that R is a ring of line type in Aff_T and gives rise to a model of synthetic differential geometry. We employ a novel theory of derivations in codifferential categories recently developed in joint work of Blute, Lucyshyn-Wright, and O'Neill.

(6) Aurore Alcolie (Lyon, France)
(Slides here)

Title: Cartesian closed 2-categories and rewriting

(Slides here)

Title: On double inverse semigroups

Abstract:
In his book, "The Theory of Inverse Semigroups", Mark Lawson describes two constructions from inverse semigroups to inductive groupoids and back again. These constructions turn out to be functorial and induce an isomorphism of categories. We extend these constructions to double inverse semigroups and double inductive groupoids -- all to be defined -- and show these constructions also determine an isomorphism of categories. We use this isomorphism to study the structure of double inverse semigroups.

(8) Bob Rosebrugh (Mount Allison, Canada)
(slides here)

Title: Asymmetric lenses, symmetric lenses, and spans

Abstract: What we now call "asymmetric lenses" were introduced about ten years  ago to provide strategies for the database "view update problem": suppose y is a (view) state derived as y=gx for a view g: X -> Y on database states X.  When can an update from y to another state y' be correctly propagated to an update x to x'?  There are several kinds of lenses depending on the database state model.

Now suppose x and y are states from model spaces X and Y and are known to be "synchronized" as witnessed by an (external) c.  How should an update to either of the states, say from x to x', be correctly propagated to an update of the other state, say from Y to y' with a resynchronization of the update state by some c'?  To adress this problem recent studies consider kinds of "symmetric" lenses.

Both asymmetric and symmetric lenses and (equivalence classes of ) symmetric lenses of the various kinds are arrows of suitable categories.  We sketch these developments and show how symmetric lenses can be generated from asymmetric lenses using the span construction.

This is joint work with Mike Johnson.

(9) Poon Lueng (Macquarie University, Australia)
(Slides here)

Title: The Free Tangent structure

Abstract:
There has been much recent work into generalizing the structures involved in the study of diﬀerential geometry.  One approach, which has been very inﬂuential, is synthetic diﬀerential geometry. Another, due to Rosicky, focused more directly on the tangent functor and its structure of (abelian) group bundle.  More recently, a further generalisation has been given by Cockett and Cruttwell, detailing a structure involving the use of additive bundles (commutative monoids). This type of structure in fact is compatible with many existing deﬁnitions of diﬀerentiability, including those used in computer science and combinatorics, the manifolds in diﬀerential and algebraic geometry and also the abstract deﬁnitions in synthetic diﬀerential geometry.

These tangent structures may be deﬁned by giving an underlying category and tangent functor with natural transformations satisfying a set of axioms. My work looks at giving an alternative; namely that these ideas of tangent structure can be captured by certain Weil algebras and the morphisms between them.  We ultimately aim to show that the resulting category of Weil algebras has tangent structure which is universal with respect to any category equipped with such structure.

(Slides here)

Title: A brief survey of some abstract machines

(slides here)

Title: Turing categories and incompleteness

Title: Universal Derivations in Codifferential Categories

Abstract: In this joint work with Richard Blute and Rory Lucyshyn-Wright, we present structural results about \emph{codifferential categories} as defined in Blute-Cockett-Seely.  Namely, it is shown that under modest hypotheses, every codifferential category is a \emph{K\"ahler category} as defined in Blute-Cockett-Porter-Seely. The proof of this fact is in striking contrast to that of the similar, conditional result in Blute-Cockett-Porter-Seely. The difference is reconciled by a novel notion of derivation for codifferential categories, with which the universal derivations of a codifferential category are shown to accord with those which were proposed in Blute-Cockett-Porter-Seely.

(Slides here)

Title: Orbifolds as manifolds

Abstract:
I will describe a join restriction category of charts and maps defined in terms of topological profunctors, and then apply the manifold  construction to obtain orbifolds.

This is joint work with Laura Scull.

Title: Working towards Andr\'e-Quillen homology

Abstract:
Almost 50 years ago, M. Andr\'e and D. Quillen independently discovered a homology theory theory for commutative rings.  The homology theory arises as a derived functor of the derivations functor and it is used extensively in commutative algebra.

About a decade ago, M.R. Kantorvicz and R. McCarthy founs that Andre-Quillen homology could be recovered as the first derivative of a particular functor using Goodwillie's calculus of functors.  However, their construction required artificially adding a base point (an object which is both initial and final).  B. Johnson, R. McCarthy and I have extended the kind of fuctor calculus used in that calculation so there is no longer a requirement for a basepoint.    One ought to be able to express Andre-Quillen homology as the first derivative of a functor again, but this time without adding a basepoint.  This was the goal of a workshop last summer, and it is work in progress by myself, M. Basterra, A. Beaudry, R. Eldred, B. Johnson, M. Merling, and S. Yeakel.  I will discuss our progress towards this result.

(17) Robin Houston (Manchester, UK)
(Slides here)

Title: No proof nets for MLL with units

MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are equivalent up to permutations. It is also, equivalently, the word problem for ∗-autonomous categories.

Previous work has shown the problem to be equivalent to a rewiring problem on proof nets, which are not canonical for full MLL due to the presence of the two units. I’ll show that MLL proof equivalence is PSPACE-complete, using a reduction from Hearn and Demaine’s Nondeterministic Constraint Logic. An important consequence of the result is that the existence of a satisfactory notion of proof nets for MLL with units is ruled out (under current complexity assumptions).

In the first session I’ll give an overview of the problem, and the reduction strategy, and try to give some intuition for the dynamics of the equivalence relation. In the second I’ll explain the construction in more detail, with the aim of at least making it reasonable for the audience to believe that the reduction works as claimed.

A reasonably complete account of the construction and proof is available here .

(slides here)

Title: An Introduction to the object-oriented calculus

Abstract:
We are quite familiar with the lambda calculus that serves as a  theoretical basis for the functional programming paradigm.  There are three other major programming paradigms, one of which is object-oriented programming (OOP).

OOP is the most popular programming paradigm in the software engineering world today as it is a natural, intuitive and powerful approach to the development of software.  It has mathematical foundations in the same way as the functional programming paradigm has; that is there is a theory of objects, the sigma-calculus, which was developed by Luca Cardelli and Martin Abadi over the 1990s.  This theory reflects, at a deeper level, the modelling issues that an object oriented programmer encounters in practice, and as such it is an important theory in the study of computer science.

The goal of this talk will be to explore the syntax and semantics of the first-order theory of objects.  In particular, we will investigate the subtyping of objects and polymorphism, and the important theoretical problem of multiple inheritance in 00P, and why it is an active field of research.

(20) Hugo Bacard (University of Western Ontario)

Title: Strictification of co-Segal dg-categories

Abstract:
Given a monoidal category {\cal M} = (M,\ox,I) we develop a theory of homotopy enriched categories with the notion of co-Segal enriched category.  Our motivation for this theory is when {\cal M} is a category of chain complexes, in which case we have what we call co-Segal dg-categories.
In this talk I  will describe the model structure on co-Segal dg-categories and show it has better properties than the model structure on strict dg-categories.  I will also show that and co-Segal dg-category is weakly equivalent to a strict dg-category.  These results hold for any  symmetric monoidal category {\cal M} (M \ox,I) whose underlying model category M is combinatorial.

(21) Robert Dawson (St Mary's University, Canada)
(Slides here)

Title: Hurewicz for Symmetric Spectra

In sufficiently nice categories of topological spaces (CW-complexes, compactly generated weak Hausdorff spaces, simplicial complexes, etc) There are two nice functors called the homotopy groups and the homology groups respectively which, conceptually, measure the number and type of holes in a given space. These functors, and variants of them, are the main objects of study in algebraic topology. There is a natural transformation between these called the hurewicz map which eases computation of these functors in some cases. All of this has been known for nearly 100 years now.

More recently, a nice extension of the category of `nice' topological spaces onto which the homotopy and homology functors extend has been brought to light by Hovey, Shipley, and Smith. In this talk I will provide an introduction to this category (the objects of which are called symmetric spectra, the extensions of homotopy and homology to this category, and the hurewicz map between them.

(23) Phil Mulry (Colgate, USA)