We introduce structures called globular multicategories with homomorphism types. We discuss how various collections of “higher category-like” objects can be used to to construct these globular multicategories. We show how to obtain a number of higher categorical structures using this data. We will see that in this setting there is a precise sense in which:
- types are higher categories,
- dependent types are profunctors,
- terms are higher functors,
- terms in a dependent context are higher transformations,
- there is a higher category of all types and terms.
This video is part of Masaryk University‘s Algebra seminar.
