Definition. Section of a Displayed Category
A section of a displayed category over chooses
- for each object , a displayed object , and
- for each morphism , a displayed morphism lying over ,
such that and .
A section is to a displayed category what a dependent function is to a dependent type: it picks a displayed datum over every base datum.