A biweekly seminar on category theory and type theory based at the University of Gothenburg and Chalmers University of Technology. The seminar is shared between the Logic and Types unit at the Computer Science Department and the Logic Group at FLoV.
The seminar takes place in the EDIT building at the Johanneberg campus. You can subscribe to our mailing list here! (If this link doesn't work, send an email to GothCat-request@lists.chalmers.se with the word "subscribe" in the subject line or body.)
Information on remote participation may appear in the future.
Sketches provide a very useful way of describing limit- and colimit-based structures in categories in a finitistic manner. Furthermore, as proven by Bastiani and Ehresmann (Bastiani and Ehresmann 1972), for any set of categories ๐, any ๐-limit sketch can be extended to a small ๐-limit theory with the same models, giving us a nice procedure for constructing limit theories. Kelly further generalised this result to the enriched setting theory when the base is locally bounded and symmetric monoidal closed categories. (Kelly 1982). Following the ideas of Makkai that axioms of structures can be captured in terms of injectivity (Makkai 1997), we reprove the theorem of Kellyโs in the case of enrichment over a locally presentable symmetric monoidal closed category. Specifically, we show that for any fixed set of weights ๐, enriched ๐-limit theories are injective objects with respect to a certain set of morphisms in the category of enriched ๐-limit sketches. Furthermore, we show that the category of ๐-limit sketches is locally presentable provided that the base of enrichment is so. By Quillenโs small object argument, we can thus construct a weak factorisation system for which the fibrant objects are ๐-limit theories. Moreover, we show that the fibrant replacement of any sketch is a theory with the same models in any ๐-complete ๐ฑ-category. Furthermore, our proof easily extends to mixed sketches. Beyond providing just another proof of the same theorem, the goal is to adapt this proof to the world of enhanced 2-sketches, as introduced in (Arkor, Bourke, and Ko 2024). In particular, we hope to show that for a sufficiently nice set of weights, the completion of an enhanced 2-sketch has the same models also when considering weaker morphisms, such as partially pseudo or lax morphisms.
I present a framework recently introduced in collaboration with Lingyuan Ye (arXiv:2504.16690) to organise and study many existing fragments of geometric logic (essentially algebraic, regular, disjunctive, coherent, and so on). The framework was recently used to deliver a modular proof of Craig interpolation that extendes to almost all finitary fragments (arXiv:2601.11221). I will also introduce open problems and some future directions.
It is easy to show that wellpointed endofunctors on (1,1)-categories can be composed. In an oo-categorical environment, this is less clear if we define a wellpointed endofunctor in a way that comes with an infinite coherence tower. In this talk, I will present a current project, which constructs for any monoidal oo-category M a monoidal structure on the oo-category M_wpt of wellpointed objects in M, which models composition of wellpointed endofunctors when M is an endofunctor category. I will also talk about various ways to construct new wellpointed objects out of old, using which one can build many interesting wellpointed endofunctors. If time permits, we show that the endofunctor (-)_wpt on the oo-category of monoidal oo-categories is a comonad, and mention some open questions, among which the classification of (-)_wpt-coalgebras.
A morphism f of a category with pullbacks is called exponentiable when base change along f has a right adjoint. This talk introduces a variation of this notion that requires a right adjoint to base change of maps belonging to a distinguished class R. To be well-behaved, such right adjoints must satisfy extra conditions. We prove the equivalence of several such conditions and say that f is R-exponentiable when these conditions hold. One application is to the interpretation of Pi types in intensional type theory. This notion also provides a general setting for a phenomenon in which two different classes of maps are exponentiable relative to each other: for instance, open and closed embeddings of topological spaces. Joint work with Joseph Hua (CMU).