Homotopy Theoretic Models of Type Theory
Peter Arndt, Chris Kapulkin
TL;DR
This paper introduces logical model categories, a class of Quillen model categories that can soundly interpret dependent types, expanding the framework for modeling type theory.
Contribution
It defines logical model categories with specific conditions that enable interpretation of dependent types, broadening the scope of models for type theory.
Findings
Logical model categories can interpret dependent products and sums.
The conditions for logical model categories are easy to verify.
A wide class of models satisfying these conditions are provided.
Abstract
We introduce the notion of a logical model category which is a Quillen model category satisfying some additional conditions. Those conditions provide enough expressive power that one can soundly interpret dependent products and sums in it. On the other hand, those conditions are easy to check and provide a wide class of models some of which are listed in the paper.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.