You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Madeleine Birchfield (Feb 06 2024 at 16:44):Given a locally cartesian closed category , is there a name for the 2-category whose objects are the slice categories of and whose morphisms are adjoint triples consisting of the base change functor, the dependent product functor, and the dependent sum functor between each slice category?
Madeleine Birchfield (Feb 06 2024 at 16:56):I think this is just called the [[categorical semantics]], although in the nLab article this is defined as a functor into the 2-category of categories rather than a particular 2-category.
Madeleine Birchfield (Feb 06 2024 at 17:09):I'm just wondering to what extent dependent type theory itself is modal type theory in which the mode theory is provided by the 2-category of slice categories.