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 [email protected] with the word "subscribe" in the subject line or body.)
Information on remote participation may appear in the future.
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).