Jon Sterling, 6 Oct 2022

The following modules develop the theory of reflective subuniverses, roughly
following the following papers:

- Rijke, Shulman, and Spitters. "Modalities in homotopy type theory". https://doi.org/10.23638/LMCS-16(1:2)2020
- Rijke. "Classifying Types: Topics in synthetic homotopy theory". PhD thesis. https://arxiv.org/abs/1906.09435

\begin{code}

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

module Modal.index where

import Modal.Open
import Modal.Subuniverse
import Modal.ReflectiveSubuniverse
import Modal.SigmaClosedReflectiveSubuniverse
import Modal.Homotopy

\end{code}