For an ordinary category and an object of , the ordinary over category satisfies the universal property that for any other category there is a natural equivalence of categories
where
denotes the category with a freely adjoined terminal object ;
denotes the category of pairs , where is a functor and is an isomorphism in .
The object can be seen as a functor . From this point of view, is a natural transformation from to , where is the inclusion functor.
Remaining in the classical setting, even more is true: is a particular case of the join operation between categories, which admits a terse description in terms of the cograph of a profunctor.
More precisely, let be two categories; their join is defined to be the category whose set of objects is the disjoint union of the sets of objects of and , and where we add one and only one morphism between any and any other . This is precisely the cograph of of the unique profunctor sending any two to the singleton.
It is extremely easy, with this definition, to show that given a functor , the category of cones over (and the category of co-cones) are uniquely characterized by the following universal properties:
where denotes the category whose objects are functors which coincide with when restricted to the full subcategory (see HTT Prop. 1.2.9.2). This characterize as a representative for the functor .
The idea of the definition of over category in the context of quasi-categories is to mimic this universal property. This relies crucially on generalizing the construction to the context of quasi-categories, in terms of the join of quasi-categories.
Fosco Loregian Warning: this paragraph is highly conjectural and for the moment I’m not able to offer any proof for these statements. In particular I would like to show
A word about the quasicategorical join operation: Joyal’s Prop. 3.1 suggests to interpret the join operation of simplicial sets as the convolution of presheaves. Nevertheless, it seems that the “pro-functorial” definition has something to say even in the -categorical case: instead of the quasicategorical model, we want to consider the simplicially enriched model for -categories. In this setting, the join of two -categories can easily be interpreted as the cograph of the terminal -profunctor sending any two objects to the terminal simplicial set.
See also this question on MO.
Therefore, let be a morphism of quasi-categories; the over-quasi-category is the quasi-category characterized by the property that for any other quasi-category there is a natural equivalence of quasi-categories
where
is the join of quasi-categories of with ;
is the quasi-category of pairs , where is a morphism of quasi-categories and is an isomorphism and is the natural inclusion.
Here one sees the advantage of having worked with the full quasi-categories of morphisms rather than with Hom-Sets. Indeed, if denotes the terminal quasi-category, then any quasi-category is naturally equivalent to .
Therefore the above description of is reduced to the following
Let be a morphism of quasi-categories. The over-quasi-category is the quasi-category .
See proposition 1.2.9.2, p. 44 and the text leading to and including proposition 1.2.9.3 of
See also chapter 3 (_Join and Slices_) in
!redirects over-category in quasi-categories?
!redirects over quasicategory?
!redirects over-quasi-category?
!redirects over-quasicategory?
!redirects overquasicategory?
!redirects slice quasi-category?
!redirects slice quasicategory?