We prove that the opposite of the category of coalgebras for the Vietoris endofunctor on the category of compact Hausdorff spaces is monadic over $\mathsf {Set}$. We deliver an analogous result for the upper, lower, and convex Vietoris endofunctors acting on the category of stably compact spaces. We provide axiomatizations of the associated (infinitary) varieties. This can be seen as a version of Jónsson–Tarski duality for modal algebras beyond the zero-dimensional setting.

C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.

The algebraic K-theory of Lawvere theories is a conceptual device to elucidate the stable homology of the symmetry groups of algebraic structures such as the permutation groups and the automorphism groups of free groups. In this paper, we fully address the question of how Morita equivalence classes of Lawvere theories interact with algebraic K-theory. On the one hand, we show that the higher algebraic K-theory is invariant under passage to matrix theories. On the other hand, we show that the higher algebraic K-theory is not fully Morita invariant because of the behavior of idempotents in non-additive contexts: We compute the K-theory of all Lawvere theories Morita equivalent to the theory of Boolean algebras.

Loday’sassembly maps approximate the K-theory of group rings by the K-theory of the coefficient ring and the corresponding homology of the group. We present a generalisation that places both ingredients on the same footing. Building on Elmendorf–Mandell’s multiplicativity results and our earlier work, we show that the K-theory of Lawvere theories is lax monoidal. This result makes it possible to present our theory in a user-friendly way without using higher-categorical language. It also allows us to extend the idea to new contexts and set up a nonabelian interpolation scheme, raising novel questions. Numerous examples illustrate the scope of our extension.

We prove that the category $\mathsf {SBor}$ of standard Borel spaces is the (bi-)initial object in the 2-category of countably complete Boolean (countably) extensive categories. This means that $\mathsf {SBor}$ is the universal category admitting some familiar algebraic operations of countable arity (e.g., countable products and unions) obeying some simple compatibility conditions (e.g., products distribute over disjoint unions). More generally, for any infinite regular cardinal $\kappa $ , the dual of the category $\kappa \mathsf {Bool}_{\kappa }$ of $\kappa $ -presented $\kappa $ -complete Boolean algebras is (bi-)initial in the 2-category of $\kappa $ -complete Boolean ( $\kappa $ -)extensive categories.

Lawvere hyperdoctrines give categorical algebraic semantics for intuitionistic predicate logic. Here we extend the hyperdoctrinal semantics to a broad variety of substructural predicate logics over the Typed Full Lambek Calculus, verifying their completeness with respect to the extended hyperdoctrinal semantics. This yields uniform hyperdoctrinal completeness results for numerous logics such as different types of relevant predicate logics and beyond, which are new results on their own; i.e., we give uniform categorical semantics for a broad variety of non-classical predicate logics. And we introduce an analogue of Lawvere–Tierney topology and cotopology in the hyperdoctrinal setting, which gives a unifying perspective on different logical translations, in particular allowing for a uniform treatment of Girard’s exponential translation between linear and intuitionistic logics and of Kolmogorov’s double negation translation between intuitionistic and classical logics. In the hyerdoctrinal conception, type theories are categories, logics over type theories are functors, and logical translations between them, then, are natural transformations, in particular Lawvere–Tierney topologies and cotopologies on hyperdoctrines. The view of logical translations as hyperdoctrinal Lawvere–Tierney topologies and cotopologies has not been elucidated before, and may be seen as a novel contribution of the present work. From a broader perspective, this work may be regarded as taking first steps towards interplay between algebraic and categorical logics; it is, technically, a combination of substructural (or Lambekian) algebraic logic and hyperdoctrinal (or Lawverian) categorical logic, as the hyperdoctrinal completeness theorem is shown via the integration of the Lindenbaum–Tarski algebra construction with the syntactic category construction. As such this work lays a foundation for further interactions between algebraic and categorical logics.

Classically, any structure for a signature ${\rm{\Sigma }}$ may be completed to a model of a desired regular theory ${T}}$ by means of the chase construction or small object argument. Moreover, this exhibits ${\rm{Mod}}\left(T)$ as weakly reflective in ${\rm{Str}}\left( {\rm{\Sigma }} \right)$.

We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e., set) models.

Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

We show that for any uncountable cardinal λ, the category of sets of cardinality at least λ and monomorphisms between them cannot appear as the category of points of a topos, in particular is not the category of models of a ${L_{\infty ,\omega }}$-theory. More generally we show that for any regular cardinal $\kappa < \lambda$ it is neither the category of κ-points of a κ-topos, in particular, nor the category of models of a ${L_{\infty ,\kappa }}$-theory.

The proof relies on the construction of a categorified version of the Scott topology, which constitute a left adjoint to the functor sending any topos to its category of points and the computation of this left adjoint evaluated on the category of sets of cardinality at least λ and monomorphisms between them. The same techniques also apply to a few other categories. At least to the category of vector spaces of with bounded below dimension and the category of algebraic closed fields of fixed characteristic with bounded below transcendence degree.

I exhibit a pair of non-symmetric operads that, while not themselves isomorphic, induce isomorphic monads. The existence of such a pair implies that if ‘algebraic theory’ is understood as meaning ‘monad’ then operads cannot be regarded as algebraic theories of a special kind.

Call a category "sketchable" if it is the category of models in sets of some sketch. This paper explores the subtle boundary between sketchable and non-sketchable categories. We show that the category of small categories that have at least one initial object and functors that take an initial object to an initial object is sketchable. The same is true for weak initial objects, but is false for subinitial objects (that every object has at most one arrow to). Analogous results hold if we substitute finite limits for terminal object. We also show that the category of groups and center-preserving homomorphisms is not sketchable. We describe briefly how "higher-order" sketches can fill these gaps.

The purpose of this note is to prove that a regular accessible category has a full regular embedding into a set-valued functor category.