| Summary: | This thesis contributes to the semantics of Martin-Lof type theory and the theory of polynomial functors. We do so by investigating polynomial functors on the category of groupoids and their initial algebras, known as W-types. We consider several versions of polynomial functors: both simple and dependent, associated to either split, cloven or general fibrations. Our main results show the existence of W-types and their pullback stability in a variety of situations. These results are obtained working constructively, ie avoiding the use of excluded middle, the axiom of choice, power set axiom, ordinal iteration. We also extend the theory of natural models, by defining a version of them for Martin-Lof type theories where eta-equality holds up to propositional, and not definitional equality.
|
|---|
