Skip to main content
To KTH's start page To KTH's start page

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

Export to calendar


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.