Jon Sterling, 16 Dec 2022

This is a nascent development of some basic 1-category theory from the univalent
point of view.

\begin{code}

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

module Categories.index where

import Categories.Category
import Categories.Functor
import Categories.NaturalTransformation
import Categories.Adjunction

\end{code}