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 Type Theory group at the Computer Science department and the Logic Group at FLoV.
Information on remote participation may appear in the future.
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).
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...). 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.