UniAgda.Everything

Table of Contents

1 Imports

{-# OPTIONS --without-K --rewriting --no-import-sorts #-}
module UniAgda.Everything where

open import UniAgda.Equiv.Inj-Surj public
open import UniAgda.Equiv.Bool public
open import UniAgda.Equiv.ClosureProperties public
open import UniAgda.Algebra.GroupTheory.basics public
open import UniAgda.HITs.PropTrunc public
open import UniAgda.HITs.0truncation public
open import UniAgda.HITs.Suspensions public
open import UniAgda.HITs.Circle public
open import UniAgda.HITs.Interval public
open import UniAgda.HITs.Core public
open import UniAgda.HITs.Pushouts public
open import UniAgda.Core.Axioms public
open import UniAgda.Core.PathAlgebra public
open import UniAgda.Core.Equivalences public
open import UniAgda.Core.Homotopy public
open import UniAgda.Core.UniversalProperties public
open import UniAgda.Core.PathSpaces.Unit public
open import UniAgda.Core.PathSpaces.Identity public
open import UniAgda.Core.PathSpaces.Sigma public
open import UniAgda.Core.PathSpaces.Coproduct public
open import UniAgda.Core.PathSpaces.Nat public
open import UniAgda.Core.SetsAndLogic.Equivalences public
open import UniAgda.Core.SetsAndLogic.Props public
open import UniAgda.Core.SetsAndLogic.Contractible public
open import UniAgda.Core.SetsAndLogic.ContrPropSet1Type public
open import UniAgda.Core.SetsAndLogic.Sets public
open import UniAgda.Core.Types.Unit public
open import UniAgda.Core.Types.Bool public
open import UniAgda.Core.Types.Identity public
open import UniAgda.Core.Types.Sigma public
open import UniAgda.Core.Types.Coproduct public
open import UniAgda.Core.Types.Nat public
open import UniAgda.Core.Types.W public
open import UniAgda.Core.Types.Functions public
open import UniAgda.Core.Types.FiniteSets public
open import UniAgda.Core.Types.Universes public
open import UniAgda.Core.Types.Empty public
open import UniAgda.Categories.Natural-Transformation public
open import UniAgda.Categories.Adjunctions public
open import UniAgda.Categories.Functor public
open import UniAgda.Categories.Category public
open import UniAgda.Categories.Equivalences public
open import UniAgda.Categories.FunctorCat public
open import UniAgda.Categories.Examples.FundamentalPregroupoid public
open import UniAgda.Categories.Examples.Group public
open import UniAgda.Categories.Examples.HomotopyPrecategory public
open import UniAgda.Categories.Examples.Initial public
open import UniAgda.Categories.Examples.Terminal public
open import UniAgda.Categories.Examples.FiniteSets public
open import UniAgda.Categories.Examples.Set public
open import UniAgda.Logic.Exists public

Author: James Leslie

Created: 2021-03-27 Sat 10:47