Algebraic models of dependent type theory

TL;DR

This paper explores algebraic and categorical frameworks for modeling dependent type theory, introducing natural models as a unifying concept with multiple perspectives and functorial semantics.

Contribution

It formalizes natural models of dependent type theory as algebraic objects, categorical morphisms, and polynomial functors, providing a comprehensive, functorial semantics.

Findings

Natural models are described as algebraic structures with operations and axioms.

They are characterized as natural transformations between presheaves.

Natural models admit interpretations of dependent type theory.

Abstract

The rules governing the essentially algebraic notion of a category with families have been observed (independently) by Steve Awodey and Marcelo Fiore to precisely match those of a representable natural transformation between presheaves. This provides us with a natural, functorial description of essentially algebraic objects which are used to model dependent type theory; following Steve Awodey, we call them 'natural models'. We can view natural models from several different viewpoints, of which we focus on three in this thesis. First, natural models are essentially algebraic, meaning that they can be described by specifying operations between sorts, subject to equational axioms; this allows us to assemble natural models into a category with certain beneficial properties. Second, since natural models are natural transformations between presheaves, they are morphisms in a locally cartesian closed category, meaning that they can be regarded as polynomials. Third, since natural models admit interpretations of dependent type theory, we can use them to provide a functorial semantics.