(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
Given a category and an object , the category of points over is the category of pointed objects of the slice category ; or alternatively the coslice-slice category
This can be unpacked the following way:
An object of is a pair of morphisms of such that is a section of ; in other words it is a split epimorphism to with a fixed choice of splitting .
A morphism is any morphism such that and .
By the construction, the category of points over is pointed and if the category has finite limits, then finitely complete; moreover the inverse image functor induced by is a left exact functor.
The category of points of has objects . In other words, the objects are the split epimorphisms of with a choice of a splitting, or equivalently the retracts in . At the level of morphisms it is just a bit more complex than the morphisms in each , namely the slice and coslice triangles become squares. More precisely, a morphism is a pair of morphisms , in such that and .
The fibration of points is the codomain-assigning functor , , . It is a fibered category in the sense of Grothendieck (cf. codomain fibration). Its fibers are the which are (as mentioned above) pointed and finitely complete. A morphism (in notation as above) is cartesian iff are the sides of a pullback square in (i.e. is a pullback of along and a pullback of along ). The inverse image functor for this fibration is exactly described by the rule above.
The notion appears in Section 3 of:
Last revised on February 8, 2023 at 15:08:51. See the history of this page for a list of all contributions to it.