A displayed structure over a category \(\mathbf{C}\) consists of

• A type family \(D : \mathbf{C}\to \mathsf{Type}\) assigning to each object \(c : \mathbf{C}\) a type \(D(c)\) of ’objects over \(c\)’;

• For each morphism \(f : I \to J\) of \(\mathbf{C}\), and objects \(x : D(I)\) and \(y : D(J)\), a type of ’morphisms from \(x\) to \(y\) over \(f\)’, denoted \(\hom _{f}({x},{y})\) or \({x} \to _{f} {y}\);

• For each \(c : \mathbf{C}\) and \(x : D(c)\), a morphism \(1_x : {x} \to _{1_c} {x}\);

• For all morphisms \(f : I \to J\) and \(g : J \to K\) in \(\mathbf{C}\) and objects \(x : D(I)\) and \(y : D(J)\) and \(z : D(K)\), a function

  \[ \hom _{f}({x},{y}) \to \hom _{g}({y},{z}) \to \hom _{f\circ {g}}({x},{z}) \, , \]

  denoted like ordinary composition by \(\bar{f}\mapsto \bar{g}\mapsto \bar{f}\circ {\bar{g}} : {x} \to _{f\circ {g}} {z}\), where \(\bar{f}: {x} \to _{f} {y}\) and \(\bar{g}: {y} \to _{g} {z}\).

A displayed category \(\mathbb {D}\) over a category \(\mathbf{C}\) is a displayed structure such that the following conditions hold:

• (Left unitality) \(1_x\circ {\bar{f}} =_{*}\bar{f}\) for all \(x : D(I)\) and \(\bar{f}: {x} \to _{f} {y}\);

• (Right unitality) \(\bar{f}\circ {1_y} =_{*}\bar{f}\) for all \(y : D(J)\) and \(\bar{f}: {x} \to _{f} {y}\);

• (Associativity) \(\bar{f}\circ {(\bar{g}\circ {\bar{h}})} =_{*}(\bar{f}\circ {\bar{g}})\circ {\bar{h}}\) for all \(\bar{f}: {x} \to _{f} {y}\), \(\bar{g}: {y} \to _{g} {z}\) and \(\bar{h}: {z} \to _{h} {w}\).

In above, the relations \(=_{*}\) are dependent equalities, over equalities of morphisms in \(\mathbf{C}\). For instance, the right unit axiom \(\bar{f}\circ {1_y} =_{*}\bar{f}\) is over the ordinary right unit axiom \(f\circ {1_b} = f\) of \(\mathbf{C}\).