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.)
Remote participation is possible by Zoom (Passcode: 606425).
If E is a real inner product space (a real vector space equipped with a bilinear, positive definite scalar product) and u is a vector in E of norm ≤ 1 (i.e. u is “small”), then the projection operator from E onto the orthogonal complement of u can be computed using an iterative construction that bears a strong resemblance to Quillen's "small object argument" for weak factorisation systems.
The goal of this talk is to show that this analogy with ℝ-modules can be extended quite far. Let 𝒱 be a locally presentable, closed symmetric monoidal category. Then the arrow category Arr(C) of any 𝒱-cocomplete 𝒱-category C has the structure of a free Arr(𝒱)-module, where Arr(𝒱) is equipped with the closed symmetric monoidal tensor product known as the “pushout-tensor". By adjointness (since 𝒱 is locally presentable), this module structure on Arr(C) equips Arr(C) with an enrichment over Arr(𝒱) (the "pullback-hom"), that is the analogue of an inner product for a vector space. This enrichment can be used to define various notions of orthogonality between morphisms of C, valued in suitably monoidal weak factorisation systems on 𝒱.
Moreover, this approach provides a generalisation of the usual notion of morphism between 𝒱-cocomplete 𝒱-categories equipped with enriched weak factorisation systems. Traditionally, such a morphism is taken to be a 𝒱-cocontinuous functor C→D that preserves the left class, but I will show how this can (and should!) be generalised to Arr(𝒱)-module morphisms Arr(C)→Arr(D) instead.
In particular, several kinds of fibrations of cubical sets (indeed, of cubical presheaves valued in any n-topos) can be characterised using enriched orthogonality, and associated enriched weak factorisation systems can be constructed for them using the enriched small object argument.
N.B. All of the results and proofs I will present are for enriched ∞-categories, and of course specialize to enriched 1-categories. I will be careful to only present constructions and arguments that can be translated to quasicategories.
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.
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.
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).