{"id":"arxiv/2607.27170","url":"https://arxiv.org/abs/2607.27170","tags":["cs.LO","math.CT"],"score":0,"title":"Free constructions for comprehension categories","domain":"cs.LO","source":"arxiv","authors":["Francesco Dagnino","Jacopo Emmenegger","Andrea Giusto"],"reviews":0,"subject":"cs.LO","summary":"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":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-29","reactions":{}}