Definition. Section of a Displayed Category

A section 𝑠 of a displayed category over π’žοΈ€ chooses

  1. for each object 𝑐:π’žοΈ€0, a displayed object , and
  2. 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.

section-of-displayed-category definition entries/displayed-category/section-of-displayed-category.hel