Internal Category with Families in Presheaves
Jason Z. S. Hu
TL;DR
This paper reviews how to construct a category with families (CwF) within presheaf categories and discusses internalizing CwF structures when the base category already has a CwF, assuming familiarity with category theory.
Contribution
It provides a method to internalize CwF structures in presheaf categories when the base category has a CwF, extending the understanding of categorical models of type theories.
Findings
Construction of CwF in presheaf categories
Internalization of CwF structures in presheaves
Assumes working knowledge of category theory
Abstract
In this note, we review a construction of category with families (CwF) in a presheaf category. When the base category of a presheaf category is a CwF, we internalize this CwF structure in the CwF of the presheaf category. This note assumes working knowledge on category theory.
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.
Taxonomy
Topicsadvanced mathematical theories