Finite Inverse Categories as Signatures

2017/07/23 by Dimitris Tsementzis, Tsementzis, Dimitris, Matthew Weaver +1
Mathematics · Computer Science · #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #Algebraic structures and combinatorial models

paper · pdf · doi:10.48550/arxiv.1707.07339

Abstract

We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.

Cited by

• First-Order Logic with Isomorphism

Related

• Categories with Dependence and Semantics of Dependent Types
• Algebraic models of dependent type theory
• Logical Structure on Inverse Functor Categories
• Type theories in category theory
• Type-Theoretic Signatures for Algebraic Theories and Inductive Types