Finite Inverse Categories as Signatures
Dimitris Tsementzis, Matthew Weaver
TL;DR
This paper introduces a dependent type theory where well-formed types are precisely characterized by finite inverse categories, establishing a formal correspondence between type theory and a specific class of categories.
Contribution
It defines a simple dependent type theory and proves an exact correspondence between its well-formed types and finite inverse categories, linking type theory with category theory.
Findings
Well-formed types correspond to finite inverse categories
Establishes a formal link between dependent type theory and category theory
Provides a foundation for categorical semantics of type theories
Abstract
We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.
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
TopicsHomotopy and Cohomology in Algebraic Topology · Logic, programming, and type systems · Algebraic structures and combinatorial models