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

{- ConnectednessAlt and the last submodule of Connection are the
   only modules importing real truncation types from the library.
   Except for that, Univalence is the only additional assumption
   to Agda MLTT we work with. -}
module Universe.index where

{- General utility funcions and type constructors for
   the pseudo-universe of types of fixed truncation level. -}
import Universe.Utility.General
import Universe.Utility.TruncUniverse

{- Pointed types.
   Corresponds to section 3 plus the first lemma of section 4,
   which used in multiple modules and thus belong here. -}
import Universe.Utility.Pointed

{- Homotopically complicated types.
   Corresponds to section 4 sans the initial lemma.
   Concludes with the main theorem that the n-types
   in the n-th universe from a strict n-type.
   Hierarchy and Trunc.* are mutually independent. -}
import Universe.Hierarchy

{- Connectedness constructions
   Corresponds to section 5.
   The first three modules develop a framework of
   truncations internal to MLTT+Univalence without truncations.
   Connection contains the main result of section 5.
   ConnectednessAlt is independent from the first four modules
   and presents a provably equivalent definition of n-connectedness
   using only propositional truncation (as remarked in the article
   and mentioned in an exercise in the HoTT book). -}
import Universe.Trunc.Universal
import Universe.Trunc.Basics
import Universe.Trunc.TypeConstructors
import Universe.Trunc.Connection
import Universe.Trunc.ConnectednessAlt