Anna Williams 14 February 2026
Notation for working with displayed categories and displayed
functors.
\begin{code}
{-# OPTIONS --safe --without-K #-}
module Categories.Displayed.Notation.index where
import Categories.Displayed.Notation.Pre
import Categories.Displayed.Notation.Univalent
\end{code}