Free constructions for comprehension categories
Logic in Computer Science
2026-07-29 v1 Category Theory
Abstract
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.
Cite
@article{arxiv.2607.27170,
title = {Free constructions for comprehension categories},
author = {Francesco Dagnino and Jacopo Emmenegger and Andrea Giusto},
journal= {arXiv preprint arXiv:2607.27170},
year = {2026}
}