Free constructions for comprehension categories

Jacobs comprehension categories subsume a large class of categorical models of type dependency, supporting also the description of morphisms between types.

We study the relationship between comprehension categories and a particular subclass, which we call Lawvere-Ehrhard comprehension categories.

First, we characterize this subclass by comparing a fibration of terms and a fibration of type morphisms associated to a given comprehension category.

Next, we provide the construction of the free comprehension category over a fibration.

Finally, we construct the free Lawvere-Ehrhard comprehension category over a Jacobs comprehension category.