Skip to main content

Michael Lindgren: Dependent products as relative adjoints

Time: Fri 2021-10-29 14.00 - 15.00

Location: Zoom: 617 9690 4048, contact to get the password

Respondent: Michael Lindgren

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.