Martin Escardo, 2018-2019 with later additions.
The lifting (aka partial-map classifier) monad.
\begin{code}
{-# OPTIONS --safe --without-K #-}
module Lifting.index where
import Lifting.Algebras
import Lifting.Construction
import Lifting.EmbeddingDirectly
import Lifting.EmbeddingViaSIP
import Lifting.IdentityViaSIP
import Lifting.Miscelanea
import Lifting.Miscelanea-PropExt-FunExt
import Lifting.Monad
import Lifting.MonadVariation
import Lifting.Set
import Lifting.Size
import Lifting.UnivalentWildCategory
import Lifting.TwoAlgebrasOnOmega
\end{code}