Till innehåll på sidan

Colin Zwanziger: Towards CwF semantics for modal dependent type theory

Tid: To 2019-11-07 kl 10.00 - 12.00

Plats: Kräftriket, house 6, room 306 (Cramér-rum)

Medverkande: Colin Zwanziger, Carnegie Mellon University

Exportera till kalender

Abstract

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.