Martin Escardo

\begin{code}

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

module Lifting.index where

import Lifting.Algebras
import Lifting.EmbeddingDirectly
import Lifting.EmbeddingViaSIP
import Lifting.IdentityViaSIP
import Lifting.Construction
import Lifting.Miscelanea
import Lifting.Miscelanea-PropExt-FunExt
import Lifting.Monad
import Lifting.MonadVariation
import Lifting.Set
import Lifting.Size
import Lifting.UnivalentPrecategory

\end{code}