Colin Zwanziger: Towards CwF semantics for modal dependent type theory
Time: Thu 2019-11-07 10.00 - 12.00
Location: Kräftriket, house 6, room 306 (Cramér-rum)
Participating: Colin Zwanziger, Carnegie Mellon University
Modal logic may be modeled using Cartesian functors and geometric morphisms between toposes (Reyes and Zolfaghari 1991, Zwanziger 2017). Analogously, modal dependent type theory may be modeled using weak morphisms and "geometric morphisms" between categories with families (CwFs), at least in a few fundamental cases (Birkedal et al. 2018, Zwanziger 2019). I illustrate one of these, giving an interpretation for an adjoint dependent type theory (cf. Krishnaswami et al. 2015) using a geometric morphism of CwFs.