Anna Williams, 28 October 2025

Formalisation of displayed categories using univalent foundations, following the
work of Ahrens and Lumsdaine [1].

[1] Ahrens, Benedikt and Peter LeFanu Lumsdaine (Mar. 2019). “Displayed
Categories”. Logical Methods in Computer Science Volume 15, Issue 1.
http://dx.doi.org/10.23638/LMCS-15(1:20)2019.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Categories.Displayed.index where

import Categories.Displayed.Pre
import Categories.Displayed.Univalent
import Categories.Displayed.Total
import Categories.Displayed.Functor

import Categories.Displayed.Notation.index

\end{code}