Globular Multicategories with Homomorphism Types

2020/05/28 by Dean, Christopher J.
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2005.14104

Abstract

We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of "higher category-like" objects such as type theories with identity types. We show how these globular multicategories can be used to construct various weak higher categorical structures of types and terms.

Related

• Concrete Categories in Homotopy Type Theory
• Weakly globular N-fold categories as a model of weak N-categories
• Multiple categories: the equivalence of a globular and a cubical approach
• Weakly globular Tamsamani N-categories and their rigidification
• An extension of Batanin's approach to globular algebras