Michael Lindgren: Dependent products as relative adjoints
Time: Fri 2021-10-29 14.00 - 15.00
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.