An inductive-recursive universe generic for small families
Logic in Computer Science
2022-02-14 v1
Abstract
We show that it is possible to construct a universe in all Grothendieck topoi with injective codes a la Pujet and Tabareau which is nonetheless generic for small families. As a trivial consequence, we show that their observational type theory admits interpretations in Grothendieck topoi suitable for use as internal languages.
Cite
@article{arxiv.2202.05529,
title = {An inductive-recursive universe generic for small families},
author = {Daniel Gratzer},
journal= {arXiv preprint arXiv:2202.05529},
year = {2022}
}