Globular Multicategories with Homomorphism Types

TL;DR

This paper introduces globular multicategories with homomorphism types, providing a framework to organize higher category-like objects such as type theories with identity types, and constructing weak higher categorical structures.

Contribution

It presents a novel notion of globular multicategories with homomorphism types for modeling higher categorical structures in type theories.

Findings

Framework for organizing higher category-like objects

Construction of weak higher categorical structures

Application to type theories with identity types

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.