Slice category
In category theory, a slice of a category 
over an object C of , written 
, is a category with
- objects as -morphisms
- morphisms from to
as those -morphisms 
for which 
.
Iterating the slicing "operation" still gives a slice of the original category (up to isomorphism).
A category is said to be locally cartesian closed if every slice of it is cartesian closed. Locally cartesian closed categories are the classifying categories of dependent type theories.
Categories: Category theory