{-# OPTIONS --cubical-compatible --safe #-}

module Everything where

import Classical
import Classical.Bundles
import Classical.Bundles.AbelianGroup
import Classical.Bundles.CommutativeMonoid
import Classical.Bundles.CommutativeRing
import Classical.Bundles.CommutativeSemigroup
import Classical.Bundles.DistributiveLattice
import Classical.Bundles.Group
import Classical.Bundles.Lattice
import Classical.Bundles.Magma
import Classical.Bundles.Monoid
import Classical.Bundles.Ring
import Classical.Bundles.Semigroup
import Classical.Bundles.Semilattice
import Classical.Categories
import Classical.Categories.AdjoinUnit
import Classical.Categories.Forgetful
import Classical.Equations
import Classical.Interpretations
import Classical.Interpretations.Maltsev
import Classical.Operations
import Classical.Properties
import Classical.Properties.Lattice
import Classical.Signatures
import Classical.Signatures.Group
import Classical.Signatures.Lattice
import Classical.Signatures.Magma
import Classical.Signatures.Monoid
import Classical.Signatures.Ring
import Classical.Small
import Classical.Small.Structures
import Classical.Small.Structures.AbelianGroup
import Classical.Small.Structures.CommutativeMonoid
import Classical.Small.Structures.CommutativeRing
import Classical.Small.Structures.CommutativeSemigroup
import Classical.Small.Structures.DistributiveLattice
import Classical.Small.Structures.Group
import Classical.Small.Structures.Lattice
import Classical.Small.Structures.Magma
import Classical.Small.Structures.Monoid
import Classical.Small.Structures.Ring
import Classical.Small.Structures.Semigroup
import Classical.Small.Structures.Semilattice
import Classical.Structures
import Classical.Structures.AbelianGroup
import Classical.Structures.CommutativeMonoid
import Classical.Structures.CommutativeRing
import Classical.Structures.CommutativeSemigroup
import Classical.Structures.DistributiveLattice
import Classical.Structures.Group
import Classical.Structures.Interpret
import Classical.Structures.Lattice
import Classical.Structures.Magma
import Classical.Structures.Monoid
import Classical.Structures.Ring
import Classical.Structures.Semigroup
import Classical.Structures.Semilattice
import Classical.Theories
import Classical.Theories.AbelianGroup
import Classical.Theories.CommutativeMonoid
import Classical.Theories.CommutativeRing
import Classical.Theories.CommutativeSemigroup
import Classical.Theories.DistributiveLattice
import Classical.Theories.Group
import Classical.Theories.Lattice
import Classical.Theories.Monoid
import Classical.Theories.Ring
import Classical.Theories.Semigroup
import Classical.Theories.Semilattice
import Demos
import Demos.ContraX
import Demos.GeneralOperationsAndRelations
import Demos.HSP
import Examples
import Examples.Classical
import Examples.Classical.CommutativeIdempotentMagma
import Examples.Classical.CommutativeMonoid
import Examples.Classical.CommutativeRing
import Examples.Classical.CommutativeSemigroup
import Examples.Classical.Groups
import Examples.Classical.Groups.AbelianGroup
import Examples.Classical.Groups.CyclicGroup
import Examples.Classical.Groups.CyclicGroup3
import Examples.Classical.Groups.KleinFourGroup
import Examples.Classical.Groups.SymmetricGroup3
import Examples.Classical.Lattices
import Examples.Classical.Lattices.L2
import Examples.Classical.Lattices.L2Distributive
import Examples.Classical.Lattices.L3Heyting
import Examples.Classical.Lattices.L7
import Examples.Classical.Magma
import Examples.Classical.Monoid
import Examples.Classical.Semigroup
import Examples.Classical.Semilattice
import Examples.FunctionTypeBijections
import Examples.PolynomialFunctors
import Examples.PolynomialFunctors.Functors
import Examples.Setoid
import Examples.Setoid.CongruenceLattice
import Examples.Setoid.FinitarySignatures
import Examples.Setoid.FiniteQuotient
import Examples.Setoid.FreeMagma
import Examples.Setoid.FreeSemigroup
import Examples.Setoid.HSPCommutativeMonoid
import Examples.Setoid.Presentation
import Examples.Setoid.SubalgebraLattice
import Examples.Setoid.SubgroupLattice
import Examples.Structures
import Examples.Structures.Basic
import Examples.Structures.Signatures
import Exercises
import Exercises.Complexity
import Exercises.Complexity.FiniteCSP
import Order
import Order.CompleteLattice
import Overture
import Overture.Adjunction
import Overture.Adjunction.Closure
import Overture.Adjunction.Galois
import Overture.Adjunction.Residuation
import Overture.Basic
import Overture.Cayley
import Overture.Functions
import Overture.Operations
import Overture.Operations.Properties
import Overture.Preface
import Overture.Relations
import Overture.Signatures
import Overture.Signatures.Morphisms
import Overture.Terms
import Overture.Terms.Basic
import Overture.Terms.Interpretation
import Overture.Terms.Translation
import Setoid
import Setoid.Algebras
import Setoid.Algebras.Basic
import Setoid.Algebras.Products
import Setoid.Algebras.Reduct
import Setoid.Categories
import Setoid.Categories.Adjunction
import Setoid.Categories.Algebra
import Setoid.Categories.Category
import Setoid.Categories.FullSubcategory
import Setoid.Categories.Functor
import Setoid.Categories.Monad
import Setoid.Categories.NaturalTransformation
import Setoid.Categories.Reduct
import Setoid.Complexity
import Setoid.Complexity.Basic
import Setoid.Complexity.CSP
import Setoid.Congruences
import Setoid.Congruences.Basic
import Setoid.Congruences.ChainJoin
import Setoid.Congruences.CompleteLattice
import Setoid.Congruences.Generation
import Setoid.Congruences.Lattice
import Setoid.Congruences.Monolith
import Setoid.Congruences.Permutability
import Setoid.Congruences.Properties
import Setoid.Functions
import Setoid.Functions.Basic
import Setoid.Functions.Bijective
import Setoid.Functions.Injective
import Setoid.Functions.Inverses
import Setoid.Functions.Surjective
import Setoid.Homomorphisms
import Setoid.Homomorphisms.Basic
import Setoid.Homomorphisms.Factor
import Setoid.Homomorphisms.HomomorphicImages
import Setoid.Homomorphisms.Isomorphisms
import Setoid.Homomorphisms.Kernels
import Setoid.Homomorphisms.Noether
import Setoid.Homomorphisms.Products
import Setoid.Homomorphisms.Properties
import Setoid.Operations
import Setoid.Operations.Properties
import Setoid.Relations
import Setoid.Relations.Continuous
import Setoid.Relations.Discrete
import Setoid.Relations.Properties
import Setoid.Relations.Quotients
import Setoid.Signatures
import Setoid.Signatures.Functor
import Setoid.Subalgebras
import Setoid.Subalgebras.Basic
import Setoid.Subalgebras.CompleteLattice
import Setoid.Subalgebras.Properties
import Setoid.Subalgebras.Subdirect
import Setoid.Subalgebras.Subdirect.Basic
import Setoid.Subalgebras.Subdirect.BirkhoffSI
import Setoid.Subalgebras.Subdirect.Finite
import Setoid.Subalgebras.Subdirect.Irreducible
import Setoid.Subalgebras.Subuniverses
import Setoid.Terms
import Setoid.Terms.Basic
import Setoid.Terms.Interpretation
import Setoid.Terms.Monad
import Setoid.Terms.Operations
import Setoid.Terms.Properties
import Setoid.Terms.Translation
import Setoid.Varieties
import Setoid.Varieties.Closure
import Setoid.Varieties.EquationalLogic
import Setoid.Varieties.FreeAlgebras
import Setoid.Varieties.FreeSubstitution
import Setoid.Varieties.HSP
import Setoid.Varieties.Interpretation
import Setoid.Varieties.Invariance
import Setoid.Varieties.Invariants
import Setoid.Varieties.Maltsev
import Setoid.Varieties.Maltsev.Basic
import Setoid.Varieties.Maltsev.Distributivity
import Setoid.Varieties.Maltsev.Modularity
import Setoid.Varieties.Maltsev.Permutability
import Setoid.Varieties.Preservation
import Setoid.Varieties.Properties
import Setoid.Varieties.Reducts
import Setoid.Varieties.SoundAndComplete
import agda-algebras