Displayed Categories as Dependent Types

Displayed category theory is the category-theoretic analogue of dependent type theory. A category plays the role of a context, and a displayed category over it the role of a dependent type in that context. The analogy extends to each construction:

Dependent type theory	Displayed category theory
context $Γ$	category $𝒞︀$
dependent type $Γ ⊢ 𝐵$	displayed category over $𝒞︀$
dependent function $(𝑎 : 𝐴) \to 𝐵 (𝑎)$	section of
context extension $Γ, 𝑥 : 𝐵$	total category and its projection
substitution $𝐵 [𝑓]$	reindexing
$Σ$ -type	displayed total category
a type not depending on its context	weakening