{-# OPTIONS --cubical --guardedness --prop --allow-unsolved-metas #-}

module Everything where

-- This file imports every module in the project. Click on
-- a module name to go to its source.

open import Algebra
open import Algebra.Construct.Cayley
open import Algebra.Construct.Cayley.OnSet
open import Algebra.Construct.Cayley.Propositional
open import Algebra.Construct.Dyck
open import Algebra.Construct.Free.Semilattice
open import Algebra.Construct.Free.Semilattice.Definition
open import Algebra.Construct.Free.Semilattice.Direct
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Extensionality
open import Algebra.Construct.Free.Semilattice.FromList
open import Algebra.Construct.Free.Semilattice.Homomorphism
open import Algebra.Construct.Free.Semilattice.Relation.Unary
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Dec
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Def
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Map
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Properties
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Dec
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Map
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Properties
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Membership
open import Algebra.Construct.Free.Semilattice.Union
open import Algebra.Construct.OrderedMonoid
open import Algebra.Construct.Sign
open import Algebra.FreeSemiring
open import Algebra.IndexedMonoid
open import Algebra.Monus
open import Algebra.Monus.Heap
open import Algebra.SemiringLiterals
open import Applicative
open import BCK
open import Categories
open import Categories.Coequalizer
open import Categories.Diagram
open import Categories.Exercises
open import Categories.Exponential
open import Categories.Functor
open import Categories.HSets
open import Categories.Product
open import Categories.Pullback
open import Categories.Pushout
open import Choose
open import Choose.Indexed
open import Classical
open import Codata.Delay
open import Codata.Heap
open import Codata.SegFix
open import Codata.Segments
open import Codata.Stream
open import Container
open import Container.Directed
open import Container.Fixpoint
open import Container.List
open import Container.List.Isomorphism
open import Container.List.Syntax
open import Container.Membership
open import Container.Polynomial
open import Container.Quotiented
open import Container.Stream
open import Control.Applicative.Levels
open import Control.Comonad.Cofree
open import Control.Comonad.IntervalHeap
open import Control.Comonad.Stepped
open import Control.Monad.Free
open import Control.Monad.Free.Eff
open import Control.Monad.Free.Effects
open import Control.Monad.Free.ListedEffects
open import Control.Monad.Free.Quotiented
open import Control.Monad.Free.Quotiented.Containers
open import Control.Monad.Free.State
open import Control.Monad.Freer
open import Control.Monad.HeapT
open import Control.Monad.HeapT.NonTransformer
open import Control.Monad.HeapT.Sized
open import Control.Monad.Levels
open import Control.Monad.Levels.Definition
open import Control.Monad.Levels.Eliminators
open import Control.Monad.Levels.Mult
open import Control.Monad.Levels.Zipping
open import Control.Monad.ListT
open import Control.Monad.State
open import Control.Monad.Weighted
open import Control.Monad.Weighted.Category
open import Control.Monad.Weighted.Cond
open import Control.Monad.Weighted.Definition
open import Control.Monad.Weighted.Depth
open import Control.Monad.Weighted.Eliminators
open import Control.Monad.Weighted.Expect
open import Control.Monad.Weighted.Free
open import Control.Monad.Weighted.Functor
open import Control.Monad.Weighted.Functor.TypeDef
open import Control.Monad.Weighted.Monad
open import Control.Monad.Weighted.Semimodule
open import Control.Monad.Weighted.Union
open import Data.AVLTree.Internal
open import Data.AVLTree.Mapping
open import Data.Array
open import Data.Array.Skew
open import Data.Bag
open import Data.Binary.FromZeroed
open import Data.Binary.Literals
open import Data.Binary.Order
open import Data.Binary.Skew
open import Data.Bits
open import Data.Bits.Equatable
open import Data.Bits.Fold
open import Data.Bits.Order
open import Data.Bits.Order.Reverse
open import Data.Bits.Strict
open import Data.Bool
open import Data.Bool.Base
open import Data.Bool.Properties
open import Data.Bool.Truth
open import Data.Braun
open import Data.Dyck.Empty
open import Data.Dyck.Except
open import Data.Dyck.Payload
open import Data.Dyck.Prog
open import Data.Dyck.Rose
open import Data.Dyck.Sized
open import Data.Empty
open import Data.Empty.Base
open import Data.Empty.Properties
open import Data.Empty.UniversePolymorphic
open import Data.Fin
open import Data.Fin.Base
open import Data.Fin.Indexed
open import Data.Fin.Indexed.Base
open import Data.Fin.Indexed.Literals
open import Data.Fin.Indexed.Properties
open import Data.Fin.Injective
open import Data.Fin.Literals
open import Data.Fin.Properties
open import Data.Fin.Sigma
open import Data.FingerTree
open import Data.Finite
open import Data.Functor
open import Data.Graph
open import Data.Heap
open import Data.Integer
open import Data.Integer.Literals
open import Data.Lift
open import Data.List
open import Data.List.Base
open import Data.List.Filter
open import Data.List.Indexing
open import Data.List.Kleene
open import Data.List.Kleene.Membership
open import Data.List.Kleene.Relation.Unary
open import Data.List.Mapping
open import Data.List.Mapping.StringMap
open import Data.List.Membership
open import Data.List.Permute
open import Data.List.Properties
open import Data.List.Relation.Binary.Lexicographic
open import Data.List.Relation.Binary.Permutation
open import Data.List.Relation.Unary
open import Data.List.Smart
open import Data.List.Sort
open import Data.List.Sort.InsertionSort
open import Data.List.Sort.MergeSort
open import Data.List.Sort.Sorted
open import Data.List.Sugar
open import Data.List.Syntax
open import Data.Maybe
open import Data.Maybe.Base
open import Data.Maybe.Monoid
open import Data.Maybe.Properties
open import Data.Maybe.Sugar
open import Data.MonoidalHeap
open import Data.MonoidalHeap.Monad
open import Data.Nat
open import Data.Nat.AbsoluteDifference
open import Data.Nat.Base
open import Data.Nat.Compare
open import Data.Nat.DivMod
open import Data.Nat.Fold
open import Data.Nat.Literals
open import Data.Nat.Order
open import Data.Nat.Properties
open import Data.Nat.Show
open import Data.Nat.WellFounded
open import Data.Permutation.NonNorm
open import Data.Permutation.Normalised
open import Data.Permutation.Normalised.Definition
open import Data.Permutation.Normalised.Group
open import Data.Permutation.Normalised.Injective
open import Data.Permutation.Normalised.Norm
open import Data.Permutation.Normalised.RoundTrip
open import Data.Permutation.Normalised.Unnorm
open import Data.Permutation.Swap
open import Data.Pi
open import Data.Pi.Base
open import Data.PolyP
open import Data.PolyP.Composition
open import Data.PolyP.Currying
open import Data.PolyP.Derivations.Levels
open import Data.PolyP.RecursionSchemes
open import Data.PolyP.Types
open import Data.PolyP.Universe
open import Data.Probability
open import Data.Product.NAry
open import Data.Queue
open import Data.RBTree
open import Data.Rational.SternBrocot
open import Data.Rational.Unnormalised
open import Data.Row
open import Data.Set
open import Data.Set.Any
open import Data.Set.Bind
open import Data.Set.Definition
open import Data.Set.Eliminators
open import Data.Set.Empty
open import Data.Set.Functor
open import Data.Set.Hom
open import Data.Set.Member
open import Data.Set.Pred
open import Data.Set.Syntax
open import Data.Set.TreeDefinition
open import Data.Set.Union
open import Data.Sigma
open import Data.Sigma.Base
open import Data.Sigma.Properties
open import Data.Sigma.Unique
open import Data.String
open import Data.Sum
open import Data.Sum.Properties
open import Data.Ternary
open import Data.Tree.Braun
open import Data.Tree.Rose
open import Data.Tuple
open import Data.Tuple.Base
open import Data.Tuple.UniverseMonomorphic
open import Data.Unit
open import Data.Unit.Properties
open import Data.Unit.UniversePolymorphic
open import Data.Vec
open import Data.Vec.Inductive
open import Data.Vec.Iterated
open import Data.Vec.Sigma
open import Demos.AgdaBasics
open import Demos.Binary
open import Demos.Cantor
open import Demos.IndexedDatatypes
open import Demos.Live
open import Demos.Printf
open import Equiv
open import Function
open import Function.Biconditional
open import Function.Fiber
open import Function.Injective
open import Function.Injective.Base
open import Function.Injective.Properties
open import Function.Isomorphism
open import Function.Reasoning
open import Function.Surjective
open import Function.Surjective.Base
open import Function.Surjective.Properties
open import Graphs
open import HITs.PropositionalTruncation
open import HITs.PropositionalTruncation.Equivalence
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation.Sugar
open import HITs.SetQuotients
open import HITs.SetQuotients.Prod
open import HLevels
open import Hyper
open import Hyper.Comonadic
open import Hyper.MonadComonadic
open import Hyper.Monadic
open import Hyper.Monadic.Example
open import Hyper.NonPositive
open import Hyper.NonStrictPositive
open import HyperFalse
open import HyperPositive
open import Inspect
open import Instance
open import Karatsuba
open import Lambda
open import Lens
open import Lens.Composition
open import Lens.Definition
open import Lens.Operators
open import Lens.Pair
open import Level
open import LexPerm
open import Literals.Number
open import Noetherian
open import Palindrome
open import Path
open import Path.Reasoning
open import PiCalc
open import Prelude
open import Relation.Binary
open import Relation.Binary.Bool
open import Relation.Binary.Construct.Bounded
open import Relation.Binary.Construct.Decision
open import Relation.Binary.Construct.LowerBound
open import Relation.Binary.Construct.On
open import Relation.Binary.Construct.UpperBound
open import Relation.Binary.Equivalence.PropHIT
open import Relation.Binary.Equivalence.PropTruncated
open import Relation.Binary.Equivalence.Reasoning
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Logic
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Discrete
open import Relation.Nullary.Discrete.FromBoolean
open import Relation.Nullary.Discrete.Properties
open import Relation.Nullary.Omniscience
open import Relation.Nullary.Stable
open import Relation.Nullary.Stable.Properties
open import Relation.Unary
open import Stack
open import Strict
open import Strict.Properties
open import Subsets
open import Testers
open import Traversable
open import TraversalsMake
open import TreeFold
open import TreeFold.Indexed
open import WellFounded
open import WellFounded.Monus