Jon Sterling and Mike Shulman, September 2023.

Arguments due to Mike Shulman, typed into Agda by Jon Sterling.

\begin{code}

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

module WildCategories.index where

import WildCategories.Base
import WildCategories.Idempotents
import WildCategories.Cones

\end{code}