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.
Antoine Van Muylder (Oct 26 2021 at 12:53):Hello. Is there a string diagram calculus out there to represent substitutions between contexts of dependent type theory?
Nathanael Arkor (Oct 26 2021 at 13:36):Dependent type theories are often modelled by finitely complete categories, and I know @Pawel Sobocinski was working on a diagrammatic calculus for finitely complete categories, so he may have some thoughts on the topic.
Robin Piedeleu (Oct 28 2021 at 08:46):@Nathanael Arkor What's a good place to learn about models of dependent types in finitely complete categories?
Ulrik Buchholtz (Oct 28 2021 at 10:29):Robin Piedeleu said:
Nathanael Arkor What's a good place to learn about models of dependent types in finitely complete categories?
I don't know if it's the best place to learn, but the paper by Clairambault and Dybjer establishes a biequivalence between finitely complete categories and the 2-category of “democratic cwfs with extensional identity types and Σ-types” (see the paper for the precise definition and the relation to dependent type theory with extensional identity types and Σ-types). The paper also has some preliminary historical notes.
For the corresponding result for finitely complete (∞,1)-categories and intensional type theory, see Kapulkin–Szumiło.
Nathanael Arkor (Oct 28 2021 at 12:11):Robin Piedeleu said:
Nathanael Arkor What's a good place to learn about models of dependent types in finitely complete categories?
I don't really have a good answer for that, unfortunately. I don't think there's one good source that contains all the relevant aspects. A starting point would be §6 of Pitts's Categorical logic. Jacobs's Categorical Logic and Type Theory is a good introduction to dependent type theory from a slightly different perspective: that of fibred categories.
Mike Shulman (Oct 28 2021 at 20:16):I kind of like Maietti's Modular correspondence between dependent type theories and categories including pretopoi and topoi.