Martin Escardo

\begin{code}

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

module Various.index where

import Various.CantorTheoremForEmbeddings -- by Jon Sterling
import Various.Dedekind
import Various.DummettDisjunction
import Various.LawvereFPT
import Various.Lumsdaine
import Various.NatIsSetWithoutUniverse    -- by Evan Cavallo
import Various.NonCollapsibleFamily
import Various.Pataraia
import Various.Pataraia-Taylor
import Various.RootsOfBooleanFunctions
import Various.Types2019
import Various.UnivalenceFromScratch

\end{code}