Tag - Monads
We extend Bourke and Garner's idempotent adjunction between monads and pretheories to the framework of ∞-categories, and exploit this to prove many classical theorems about monads in the ∞-categorical setting. Among other things, we prove that the category of algebras for an accessible monad on a locally presentable ∞ category is locally presentable. We also apply the result to construct examples of ∞-categorical monads from pretheories.
There have traditionally been two ways to reason about universal algebraic structure categorically: via algebraic theories, and via monads. It is well known that the two are tightly related: in particular, there is a correspondence between algebraic theories and a class of monads on the category of sets.
Motivated by the study of simple type theories, Fiore and Mahmoud introduced second-order algebraic theories, which extend classical (first-order) algebraic theories by variable-binding operators, such as the existential quantifier ∃x of first-order logic; the differential operators d/dx of analysis; and the λ-abstraction operator of the unityped λ-calculus. Fiore and Mahmoud established a correspondence between second-order algebraic theories and a second-order equational logic, but did not pursue a general understanding of the categorical structure of second-order algebraic theories. In particular, the possibility of a monad–theory correspondence for second-order algebraic theories was left as an open question.
In this talk, I will present a generalization of algebraic theories to higher-order structure, in particular subsuming the second-order algebraic theories of Fiore and Mahmoud, and describe a universal property of the category of nth-order algebraic theories. The central result is a correspondence between (n+1)th-order algebraic theories and a class of relative monads on the category of nth-order algebraic theories, which extends to a monad correspondence subsuming that of the classical setting. Finally, I will discuss how the perspective lent by higher-order algebraic theories sheds new light on the classical monad-theory correspondence.
Mardare, Panangaden and Plotkin introduced C-varieties of algbebras on metric spaces. These are categories of metric-enriched algebras specified by equations in a context. A context puts restrictions on the distances of variables one uses. We prove that C-varieties are precisely the monadic categories over Met for countably accessible enriched monads preserving epimorphisms.
We analogously introduce C-varieties of ordered algebras as categories specified by inequalities in a context. Which means that conditions on inequalities between variables are imposed. We prove that C-varieties precisely correspond to enriched finitary monads on Pos preserving epimorphisms.
For S a set, S-sorted algebraic (or 'Lawvere') theories are, equivalently, finite-product categories whose objects are freely generated by S, finitary monads on Set/S, or monoids in a category of 'S-coloured cartesian collections'.
When S is a suitable direct category, I will describe equivalences of categories between finitary monads on [Sop, Set], monoids in a category of 'S-coloured cartesian collections', and a certain category of contextual categories (in the sense of Cartmell) under Sop.
Examples of such S are the categories of semi-simplices, globes and opetopes. Opetopes will be a running example, and we will see that there are three idempotent finitary monads on the category of opetopic sets, whose algebras are, respectively, small categories, coloured planar Set-operads, and planar coloured combinads (in the sense of Loday).
The notion of a distributive law of monads was introduced by Beck, and gives a concise description of the data required to compose monads. In the 2-dimensional case, Marmolejo defined pseudodistributive laws of pseudomonads (where the required diagrams only commute up to an invertible modification). However, this description requires a number of coherence conditions due to the extra data involved.
In this talk we give alternative definitions of distributive laws and pseudodistributive laws involving the decagonal coherence conditions which naturally arise when the involved monads and pseudomonads are presented in their extensive form. As an application, we show that of Marmolejo and Wood’s eight coherence axioms for pseudodistributive laws, three are redundant.
We will then go on to give (likely) minimal definitions of distributive laws and pseudodistributive laws, which further simply the coherence conditions involved in this extensive viewpoint.
One way of interpreting a left Kan extension is as taking a kind of 'partial colimit', where one replaces parts of a diagram by their colimits. We make this intuition precise by means of the 'partial evaluations' sitting in the so-called bar construction of monads. The (pseudo)monads of interest for forming colimits are the monad of diagrams and the monad of small presheaves, both on the category CAT of locally small categories. We also define a morphism of monads between them, which we call 'image', and which takes the 'free colimit' of a diagram. This morphism allows us in particular to generalize the idea of 'cofinal functors', i.e. of functors which leave colimits invariant in an absolute way. This generalization includes the concept of absolute colimit as a special case. The main result of this work says that a pointwise left Kan extension of a diagram corresponds precisely to a partial evaluation of its colimit. This categorical result is analogous to what happens in the case of probability monads, where a conditional expectation of a random variable corresponds to a partial evaluation of its centre of mass.
We develop universal algebra over an enriched category and relate it to finitary enriched monads. Using it, we deduce recent results about ordered universal algebra where inequations are used instead of equations. Then we apply it to metric universal algebra where quantitative equations are used instead of equations. This contributes to understanding of finitary monads on the category of metric spaces.
Martin Bidlingmaier: Model categories of lcc categories and the gros model of dependent type theory.
In this talk we discuss various model categories of locally cartesian closed (lcc) categories and their relevance to coherence problems, in particular the coherence problem of categorical semantics of dependent type theory. We begin with Lcc, the model category of locally cartesian closed (lcc) sketches. Its fibrant objects are precisely the lcc categories, though without assigned choices of universal objects. We then obtain a Quillen equivalent model category sLcc of strict lcc categories as the category of algebraically fibrant objects of Lcc. Strict lcc categories are categories with assigned choice of lcc structure, and their morphisms preserve these choices on the nose. Conjecturally, sLcc is precisely Lack’s model category of algebras for a 2-monad T , where T is instantiated with the free lcc category functor on Cat. We then discuss the category of algebraically cofibrant objects of sLcc and show how it can serve as a "gros" model of dependent type theory.
You must be logged in to post a comment.