Till innehåll på sidan

Michael Lindgren: Dependent products as relative adjoints

Tid: Fr 2021-10-29 kl 14.00 - 15.00

Plats: Zoom: 617 9690 4048, contact arias@math.su.se to get the password

Respondent: Michael Lindgren

Exportera till kalender

Abstract: Universal quantification in logic correspond, in categorical models, to right adjoints to weakening. However, in certain weak models of dependent type theory, known as comprehension categories, this is not always the case.

In dependent type theory, universal quantification is given by the dependent product type. In some comprehension categories, those called full, dependent products do correspond to right adjoints to weakening, but this does not hold in general.

In this thesis we present a new description of dependent products in comprehension categories as relative adjoints, and show that this holds in arbitrary comprehension categories.