Jonathan Sterling

The goal of these modules is to study the coslice (∞,1)-category of a universe
under a given type. We cannot formalize the entirety of this concept in the
current univalent foundations, but we nonetheless can do things like
characterize path spaces, etc.

\begin{code}

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

module Coslice.index where

import Coslice.Type
import Coslice.Hom

\end{code}