Håkon Robbestad Gylterud: Categories with definitions

Abstract: Making definitions is an essential part of mathematics. However, definitions are often seen as semantically irrelevant since one can always replace a defined term with its definition. In this seminar we will explore a notion of definition which *has* semantic content by relating the notion of «definition» with the notion of «construction» in the context of dependent type theory.

In concrete terms we will define «categories with definitions». It will be a variation (extra structure) on «categories with attributes», a well established notion of semantics of Martin-Löf type theory. Our main result will be to exhibit an adjunction between categories with
attributes and categories with definitions.

One distinguishing feature of these structures is that the category can remain locally finite, even though there are types with infinitely many terms – giving categories with definitions a finitist flavour.