works on
categorical semantics 1comprehension categories 1fibrations 1free constructions 1lawvere-ehrhard 1type theory 1

From the 1 of 1 linked paper with an AI index.

collaborators
Showing cs.LOShow all

1 paper · 1 filter

cs.LO2026

Free constructions for comprehension categories

Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto

The paper investigates comprehension categories used to model type dependency, introduces a subclass called Lawvere‑Ehrhard comprehension categories, and provides constructions of…