{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module UF.index where

import UF.Base
import UF.Choice
import UF.Classifiers
import UF.Classifiers-Old
import UF.Connected
import UF.CumulativeHierarchy               -- by de Jong, Kraus, Nordvall Forsberg and Xu.
import UF.CumulativeHierarchy-LocallySmall  -- by de Jong, Kraus, Nordvall Forsberg and Xu.
import UF.Embeddings
import UF.Equiv
import UF.Equiv-FunExt
import UF.EquivalenceExamples
import UF.ExcludedMiddle
import UF.FunExt
import UF.FunExt-Properties
import UF.FunExt-from-Naive-FunExt
import UF.Groupoids
import UF.IdEmbedding
import UF.IdentitySystems
import UF.ImageAndSurjection
import UF.ImageAndSurjection-F
import UF.Knapp-UA
import UF.KrausLemma
import UF.Large-Quotient
import UF.LeftCancellable
import UF.Logic
import UF.Lower-FunExt
import UF.Miscelanea
import UF.PairFun
import UF.Powerset
import UF.Powerset-Fin
import UF.Powerset-Resizing
import UF.PreSIP
import UF.PreSIP-Examples
import UF.PreUnivalence
import UF.PropIndexedPiSigma
import UF.PropTrunc
import UF.PropTrunc-F
import UF.Quotient
import UF.Quotient-F
import UF.Quotient-Replacement
import UF.Retracts
import UF.Retracts-FunExt
import UF.SIP
import UF.SIP-Examples
import UF.Section-Embedding
import UF.SetTrunc
import UF.Size
import UF.SmallnessProperties
import UF.StructureIdentityPrinciple -- obsolete but keep
import UF.Subsingletons
import UF.Subsingletons-FunExt
import UF.UA-FunExt
import UF.Univalence
import UF.UniverseEmbedding
import UF.Yoneda
import UF.hlevels