On homotopy exponentials in path categories

TL;DR

This paper explores the enrichment of path categories over groupoids and introduces new notions of homotopy exponential and Pi-type, establishing their properties and technical foundations within this enriched framework.

Contribution

It introduces the concepts of strong homotopy exponential and Pi-type for path categories, expanding the theoretical understanding of their structure and properties.

Findings

Path categories are shown to be enriched over groupoids.

Introduces strong homotopy exponential and Pi-type notions.

Establishes basic properties and technical propositions for these new concepts.

Abstract

In the first part of this paper we show that path categories are enriched over groupoids, in a way that is compatible with a suitable 2-category of path categories. In the second part we introduce a new notion of homotopy exponential and homotopy Pi-type for path categories, the strong homotopy exponential and the strong homotopy Pi-type. We prove some of their basic properties, along with two important technical propositions. The results in the second part of this paper are mostly obtained using the groupoid enrichment of path categories established in the first part.