    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- All library modules, along with short descriptions
    ------------------------------------------------------------------------

    -- Note that core modules are not included.

    {-# OPTIONS --safe --guardedness #-}

    module EverythingSafe where

    -- Definitions of algebraic structures like monoids and rings
    -- (packed in records together with sets, operations, etc.)
    import Algebra

    -- Algebraic objects with an apartness relation
    import Algebra.Apartness

    -- Bundles for local algebraic structures
    import Algebra.Apartness.Bundles

    -- Properties of Heyting Commutative Rings
    import Algebra.Apartness.Properties.HeytingCommutativeRing

    -- Algebraic structures with an apartness relation
    import Algebra.Apartness.Structures

    -- Definitions of algebraic structures like monoids and rings
    -- (packed in records together with sets, operations, etc.)
    import Algebra.Bundles

    -- Definitions of 'raw' bundles
    import Algebra.Bundles.Raw

    -- Lemmas relating algebraic definitions (such as associativity and
    -- commutativity) that don't require the equality relation to be a setoid.
    import Algebra.Consequences.Base

    -- Relations between properties of functions, such as associativity and
    -- commutativity (specialised to propositional equality)
    import Algebra.Consequences.Propositional

    -- Relations between properties of functions, such as associativity and
    -- commutativity, when the underlying relation is a setoid
    import Algebra.Consequences.Setoid

    -- Definition of algebraic structures we get from freely adding an
    -- identity element
    import Algebra.Construct.Add.Identity

    -- Instances of algebraic structures made by taking two other instances
    -- A and B, and having elements of the new instance be pairs |A| × |B|.
    -- In mathematics, this would usually be written A × B or A ⊕ B.
    import Algebra.Construct.DirectProduct

    -- Flipping the arguments of a binary operation preserves many of its
    -- algebraic properties.
    import Algebra.Construct.Flip.Op

    -- Instances of algebraic structures where the carrier is ⊥.
    -- In mathematics, this is usually called 0.
    import Algebra.Construct.Initial

    -- Definitions of the lexicographic product of two operators.
    import Algebra.Construct.LexProduct

    -- Definitions of the lexicographic product of two operators.
    import Algebra.Construct.LexProduct.Base

    -- Properties of the inner lexicographic product of two operators.
    import Algebra.Construct.LexProduct.Inner

    -- Choosing between elements based on the result of applying a function
    import Algebra.Construct.LiftedChoice

    -- Basic definition of an operator that computes the min/max value
    -- with respect to a total preorder.
    import Algebra.Construct.NaturalChoice.Base

    -- The max operator derived from an arbitrary total preorder.
    import Algebra.Construct.NaturalChoice.Max

    -- Properties of a max operator derived from a spec over a total
    -- preorder.
    import Algebra.Construct.NaturalChoice.MaxOp

    -- The min operator derived from an arbitrary total preorder.
    import Algebra.Construct.NaturalChoice.Min

    -- Properties of min and max operators specified over a total
    -- preorder.
    import Algebra.Construct.NaturalChoice.MinMaxOp

    -- Properties of a min operator derived from a spec over a total
    -- preorder.
    import Algebra.Construct.NaturalChoice.MinOp

    -- For each `IsX` algebraic structure `S`, lift the structure to the
    -- 'pointwise' function space `A → S`: categorically, this is the
    -- *power* object in the relevant category of `X` objects and morphisms
    import Algebra.Construct.Pointwise

    -- Substituting equalities for binary relations
    import Algebra.Construct.Subst.Equality

    -- Instances of algebraic structures where the carrier is ⊤. In
    -- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
    import Algebra.Construct.Terminal

    -- Instances of algebraic structures where the carrier is ⊤. In
    -- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
    import Algebra.Construct.Zero

    -- Properties of functions, such as associativity and commutativity
    import Algebra.Definitions

    -- Basic auxiliary definitions for magma-like structures
    import Algebra.Definitions.RawMagma

    -- Basic auxiliary definitions for monoid-like structures
    import Algebra.Definitions.RawMonoid

    -- Basic auxiliary definitions for semiring-like structures
    import Algebra.Definitions.RawSemiring

    -- This module is DEPRECATED.
    import Algebra.FunctionProperties.Consequences

    -- This module is DEPRECATED.
    import Algebra.FunctionProperties.Consequences.Propositional

    -- Definitions of algebraic structures like semilattices and lattices
    -- (packed in records together with sets, operations, etc.), defined via
    -- meet/join operations and their properties
    import Algebra.Lattice

    -- Definitions of algebraic structures like semilattices and lattices
    -- (packed in records together with sets, operations, etc.), defined via
    -- meet/join operations and their properties
    import Algebra.Lattice.Bundles

    -- Definitions of 'raw' bundles
    import Algebra.Lattice.Bundles.Raw

    -- Instances of algebraic structures made by taking two other instances
    -- A and B, and having elements of the new instance be pairs |A| × |B|.
    -- In mathematics, this would usually be written A × B or A ⊕ B.
    import Algebra.Lattice.Construct.DirectProduct

    -- Choosing between elements based on the result of applying a function
    import Algebra.Lattice.Construct.LiftedChoice

    -- Properties of a max operator derived from a spec over a total
    -- preorder.
    import Algebra.Lattice.Construct.NaturalChoice.MaxOp

    -- Properties of min and max operators specified over a total preorder.
    import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp

    -- Properties of a min operator derived from a spec over a total
    -- preorder.
    import Algebra.Lattice.Construct.NaturalChoice.MinOp

    -- Substituting equalities for binary relations
    import Algebra.Lattice.Construct.Subst.Equality

    -- Instances of algebraic lattice structures where the carrier is ⊤.
    -- In mathematics, this is usually called 0.
    import Algebra.Lattice.Construct.Zero

    -- Morphisms between algebraic lattice structures
    import Algebra.Lattice.Morphism

    -- The composition of morphisms between algebraic lattice structures.
    import Algebra.Lattice.Morphism.Construct.Composition

    -- The identity morphism for algebraic lattice structures
    import Algebra.Lattice.Morphism.Construct.Identity

    -- Consequences of a monomorphism between lattice-like structures
    import Algebra.Lattice.Morphism.LatticeMonomorphism

    -- Morphisms between algebraic lattice structures
    import Algebra.Lattice.Morphism.Structures

    -- Some derivable properties of Boolean algebras
    import Algebra.Lattice.Properties.BooleanAlgebra

    -- Boolean algebra expressions
    import Algebra.Lattice.Properties.BooleanAlgebra.Expression

    -- Some derivable properties
    import Algebra.Lattice.Properties.DistributiveLattice

    -- Some derivable properties of lattices
    import Algebra.Lattice.Properties.Lattice

    -- Some derivable properties of semilattices
    import Algebra.Lattice.Properties.Semilattice

    -- Some lattice-like structures defined by properties of _∧_ and _∨_
    -- (not packed up with sets, operations, etc.)
    import Algebra.Lattice.Structures

    -- Some biased records for lattice-like structures. Such records are
    -- often easier to construct, but are suboptimal to use more widely and
    -- should be converted to the standard record definitions immediately
    -- using the provided conversion functions.
    import Algebra.Lattice.Structures.Biased

    -- Definitions of algebraic structure module
    -- packed in records together with sets, operations, etc.
    import Algebra.Module

    -- Definitions of algebraic structures defined over some other
    -- structure, like modules and vector spaces
    import Algebra.Module.Bundles

    -- Definitions of 'raw' bundles for module-like algebraic structures
    import Algebra.Module.Bundles.Raw

    -- Relations between properties of scaling and other operations
    import Algebra.Module.Consequences

    -- This module constructs the biproduct of two R-modules, and similar
    -- for weaker module-like structures.
    -- The intended universal property is that the biproduct is both a
    -- product and a coproduct in the category of R-modules.
    import Algebra.Module.Construct.DirectProduct

    -- The non-commutative analogue of Nagata's construction of
    -- the "idealization of a module", (Local Rings, 1962; Wiley)
    -- defined here on R-R-*bi*modules M over a ring R, as used in
    -- "Forward- or reverse-mode automatic differentiation: What's the difference?"
    -- (Van den Berg, Schrijvers, McKinna, Vandenbroucke;
    -- Science of Computer Programming, Vol. 234, January 2024
    -- https://doi.org/10.1016/j.scico.2023.103010)
    import Algebra.Module.Construct.Idealization

    -- This module constructs the unit of the monoidal structure on
    -- R-modules, and similar for weaker module-like structures.
    -- The intended universal property is that the maps out of the tensor
    -- unit into M are isomorphic to the elements of M.
    import Algebra.Module.Construct.TensorUnit

    -- This module constructs the zero R-module, and similar for weaker
    -- module-like structures.
    -- The intended universal property is that, given any R-module M, there
    -- is a unique map into and a unique map out of the zero R-module
    -- from/to M.
    import Algebra.Module.Construct.Zero

    -- This module collects the property definitions for left-scaling
    -- (LeftDefs), right-scaling (RightDefs), and both (BiDefs).
    import Algebra.Module.Definitions

    -- Properties connecting left-scaling and right-scaling
    import Algebra.Module.Definitions.Bi

    -- Properties connecting left-scaling and right-scaling over the same scalars
    import Algebra.Module.Definitions.Bi.Simultaneous

    -- Properties of left-scaling
    import Algebra.Module.Definitions.Left

    -- Properties of right-scaling
    import Algebra.Module.Definitions.Right

    -- Properties of a monomorphism between bimodules
    import Algebra.Module.Morphism.BimoduleMonomorphism

    -- Consequences of a monomorphism between bisemimodules
    import Algebra.Module.Morphism.BisemimoduleMonomorphism

    -- The composition of morphisms between module-like algebraic structures.
    import Algebra.Module.Morphism.Construct.Composition

    -- The identity morphism for module-like algebraic structures
    import Algebra.Module.Morphism.Construct.Identity

    -- Basic definitions for morphisms between module-like algebraic
    -- structures
    import Algebra.Module.Morphism.Definitions

    -- Consequences of a monomorphism between left modules
    import Algebra.Module.Morphism.LeftModuleMonomorphism

    -- Consequences of a monomorphism between left semimodules
    import Algebra.Module.Morphism.LeftSemimoduleMonomorphism

    -- Properties of linear maps.
    import Algebra.Module.Morphism.ModuleHomomorphism

    -- Consequences of a monomorphism between modules
    import Algebra.Module.Morphism.ModuleMonomorphism

    -- Consequences of a monomorphism between right modules
    import Algebra.Module.Morphism.RightModuleMonomorphism

    -- Consequences of a monomomorphism between right semimodules
    import Algebra.Module.Morphism.RightSemimoduleMonomorphism

    -- Properties of a monomorphism between semimodules
    import Algebra.Module.Morphism.SemimoduleMonomorphism

    -- Morphisms between module-like algebraic structures
    import Algebra.Module.Morphism.Structures

    -- Properties of modules.
    import Algebra.Module.Properties

    -- Properties of bimodules.
    import Algebra.Module.Properties.Bimodule

    -- Properties of left modules.
    import Algebra.Module.Properties.LeftModule

    -- Properties of right modules.
    import Algebra.Module.Properties.RightModule

    -- Properties of semimodules.
    import Algebra.Module.Properties.Semimodule

    -- Some algebraic structures defined over some other structure
    import Algebra.Module.Structures

    -- This module provides alternative ways of providing instances of
    -- structures in the Algebra.Module hierarchy.
    import Algebra.Module.Structures.Biased

    -- Morphisms between algebraic structures
    import Algebra.Morphism

    -- Bundled definitions of homomorphisms between algebras
    import Algebra.Morphism.Bundles

    -- Some properties of Magma homomorphisms
    import Algebra.Morphism.Consequences

    -- The composition of morphisms between algebraic structures.
    import Algebra.Morphism.Construct.Composition

    -- The projection morphisms for algebraic structures arising from the
    -- direct product construction
    import Algebra.Morphism.Construct.DirectProduct

    -- The identity morphism for algebraic structures
    import Algebra.Morphism.Construct.Identity

    -- The unique morphism from the initial object,
    -- for each of the relevant categories. Since
    -- `Semigroup` and `Band` are simply `Magma`s
    -- satisfying additional properties, it suffices to
    -- define the morphism on the underlying `RawMagma`.
    import Algebra.Morphism.Construct.Initial

    -- The unique morphism to the terminal object,
    -- for each of the relevant categories. Since
    -- each terminal algebra builds on `Monoid`,
    -- possibly with additional (trivial) operations,
    -- satisfying additional properties, it suffices to
    -- define the morphism on the underlying `RawMonoid`
    import Algebra.Morphism.Construct.Terminal

    -- Basic definitions for morphisms between algebraic structures
    import Algebra.Morphism.Definitions

    -- Consequences of a monomorphism between group-like structures
    import Algebra.Morphism.GroupMonomorphism

    -- Consequences of a monomorphism between magma-like structures
    import Algebra.Morphism.MagmaMonomorphism

    -- Consequences of a monomorphism between monoid-like structures
    import Algebra.Morphism.MonoidMonomorphism

    -- Consequences of a monomorphism between ring-like structures
    import Algebra.Morphism.RingMonomorphism

    -- Morphisms between algebraic structures
    import Algebra.Morphism.Structures

    -- This module is DEPRECATED.
    import Algebra.Operations.CommutativeMonoid

    -- This module is DEPRECATED.
    import Algebra.Operations.Ring

    -- This module is DEPRECATED.
    import Algebra.Operations.Semiring

    -- Some derivable properties
    import Algebra.Properties.AbelianGroup

    -- This module is DEPRECATED.
    import Algebra.Properties.BooleanAlgebra

    -- This module is DEPRECATED.
    import Algebra.Properties.BooleanAlgebra.Expression

    -- Some properties of operations in CancellativeCommutativeSemiring.
    import Algebra.Properties.CancellativeCommutativeSemiring

    -- Properties of divisibility over commutative magmas
    import Algebra.Properties.CommutativeMagma.Divisibility

    -- Some derivable properties
    import Algebra.Properties.CommutativeMonoid

    -- Multiplication over a monoid (i.e. repeated addition)
    import Algebra.Properties.CommutativeMonoid.Mult

    -- Multiplication over a monoid (i.e. repeated addition) optimised for
    -- type checking.
    import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised

    -- Finite summations over a commutative monoid
    import Algebra.Properties.CommutativeMonoid.Sum

    -- Some theory for commutative semigroup
    import Algebra.Properties.CommutativeSemigroup

    -- Properties of divisibility over commutative semigroups
    import Algebra.Properties.CommutativeSemigroup.Divisibility

    -- The Binomial Theorem for Commutative Semirings
    import Algebra.Properties.CommutativeSemiring.Binomial

    -- Exponentiation defined over a commutative semiring as repeated multiplication
    import Algebra.Properties.CommutativeSemiring.Exp

    -- Exponentiation over a semiring optimised for type-checking.
    import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised

    -- This module is DEPRECATED.
    import Algebra.Properties.DistributiveLattice

    -- Some derivable properties
    import Algebra.Properties.Group

    -- Some derivable properties
    import Algebra.Properties.IdempotentCommutativeMonoid

    -- Some derivable properties
    import Algebra.Properties.KleeneAlgebra

    -- This module is DEPRECATED. Please use
    -- `Algebra.Lattice.Properties.Lattice` instead.
    import Algebra.Properties.Lattice

    -- Some basic properties of Loop
    import Algebra.Properties.Loop

    -- Divisibility over magmas
    import Algebra.Properties.Magma.Divisibility

    -- Some basic properties of Quasigroup
    import Algebra.Properties.MiddleBolLoop

    -- Equational reasoning for monoids
    -- (Utilities for identity and cancellation reasoning, extending semigroup reasoning)
    import Algebra.Properties.Monoid

    -- Properties of divisibility over monoids
    import Algebra.Properties.Monoid.Divisibility

    -- Multiplication over a monoid (i.e. repeated addition)
    import Algebra.Properties.Monoid.Mult

    -- Multiplication over a monoid (i.e. repeated addition) optimised for
    -- type checking.
    import Algebra.Properties.Monoid.Mult.TCOptimised

    -- Finite summations over a monoid
    import Algebra.Properties.Monoid.Sum

    -- Some derivable properties
    import Algebra.Properties.MoufangLoop

    -- Some basic properties of Quasigroup
    import Algebra.Properties.Quasigroup

    -- Some basic properties of Rings
    import Algebra.Properties.Ring

    -- Some basic properties of RingWithoutOne
    import Algebra.Properties.RingWithoutOne

    -- Some theory for Semigroup
    import Algebra.Properties.Semigroup

    -- Properties of divisibility over semigroups
    import Algebra.Properties.Semigroup.Divisibility

    -- This module is DEPRECATED. Please use
    -- `Algebra.Lattice.Properties.Semilattice` instead.
    import Algebra.Properties.Semilattice

    -- The Binomial Theorem for *-commuting elements in a Semiring
    import Algebra.Properties.Semiring.Binomial

    -- Properties of divisibility over semirings
    import Algebra.Properties.Semiring.Divisibility

    -- Exponentiation defined over a semiring as repeated multiplication
    import Algebra.Properties.Semiring.Exp

    -- Exponentiation over a semiring optimised for type-checking.
    import Algebra.Properties.Semiring.Exp.TCOptimised

    -- Exponentiation over a semiring optimised for tail-recursion.
    import Algebra.Properties.Semiring.Exp.TailRecursiveOptimised

    -- Multiplication by a natural number over a semiring
    import Algebra.Properties.Semiring.Mult

    -- Multiplication over a semiring optimised for type-checking.
    import Algebra.Properties.Semiring.Mult.TCOptimised

    -- Properties of Coprimality and Irreducibility for Semiring.
    import Algebra.Properties.Semiring.Primality

    -- Finite summations over a semiring
    import Algebra.Properties.Semiring.Sum

    -- Solver for equations in commutative monoids
    import Algebra.Solver.CommutativeMonoid

    -- An example of how Algebra.CommutativeMonoidSolver can be used
    import Algebra.Solver.CommutativeMonoid.Example

    -- Normal forms in commutative monoids
    import Algebra.Solver.CommutativeMonoid.Normal

    -- Solver for equations in idempotent commutative monoids
    import Algebra.Solver.IdempotentCommutativeMonoid

    -- An example of how Algebra.IdempotentCommutativeMonoidSolver can be
    -- used
    import Algebra.Solver.IdempotentCommutativeMonoid.Example

    -- Solver for equations in idempotent commutative monoids
    import Algebra.Solver.IdempotentCommutativeMonoid.Normal

    -- A solver for equations over monoids
    import Algebra.Solver.Monoid

    -- A solver for equations over monoids
    import Algebra.Solver.Monoid.Expression

    -- A solver for equations over monoids
    import Algebra.Solver.Monoid.Normal

    -- A solver for equations over monoids
    import Algebra.Solver.Monoid.Solver

    -- Old solver for commutative ring or semiring equalities
    import Algebra.Solver.Ring

    -- Commutative semirings with some additional structure ("almost"
    -- commutative rings), used by the ring solver
    import Algebra.Solver.Ring.AlmostCommutativeRing

    -- Some boring lemmas used by the ring solver
    import Algebra.Solver.Ring.Lemmas

    -- Instantiates the ring solver, using the natural numbers as the
    -- coefficient "ring"
    import Algebra.Solver.Ring.NaturalCoefficients

    -- Instantiates the natural coefficients ring solver, using coefficient
    -- equality induced by ℕ.
    import Algebra.Solver.Ring.NaturalCoefficients.Default

    -- Instantiates the ring solver with two copies of the same ring with
    -- decidable equality
    import Algebra.Solver.Ring.Simple

    -- Some algebraic structures (not packed up with sets, operations, etc.)
    import Algebra.Structures

    -- Ways to give instances of certain structures where some fields can
    -- be given in terms of others. Re-exported via `Algebra`.
    import Algebra.Structures.Biased

    -- Results concerning double negation elimination.
    import Axiom.DoubleNegationElimination

    -- Results concerning the excluded middle axiom.
    import Axiom.ExcludedMiddle

    -- Results concerning function extensionality for propositional equality
    import Axiom.Extensionality.Heterogeneous

    -- Results concerning function extensionality for propositional equality
    import Axiom.Extensionality.Propositional

    -- Results concerning uniqueness of identity proofs
    import Axiom.UniquenessOfIdentityProofs

    -- Results concerning uniqueness of identity proofs, with axiom K
    import Axiom.UniquenessOfIdentityProofs.WithK

    -- M-types (the dual of W-types)
    import Codata.Guarded.M

    -- Infinite streams defined as coinductive records
    import Codata.Guarded.Stream

    -- Properties of infinite streams defined as coinductive records
    import Codata.Guarded.Stream.Properties

    -- Coinductive pointwise lifting of relations to streams
    import Codata.Guarded.Stream.Relation.Binary.Pointwise

    -- Streams where all elements satisfy a given property
    import Codata.Guarded.Stream.Relation.Unary.All

    -- Streams where at least one element satisfies a given property
    import Codata.Guarded.Stream.Relation.Unary.Any

    -- "Finite" sets indexed on coinductive "natural" numbers
    import Codata.Musical.Cofin

    -- Coinductive "natural" numbers
    import Codata.Musical.Conat

    -- Coinductive "natural" numbers: base type and operations
    import Codata.Musical.Conat.Base

    -- M-types (the dual of W-types)
    import Codata.Musical.M

    -- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
    -- trees).
    import Codata.Musical.M.Indexed

    -- Basic types related to coinduction
    import Codata.Musical.Notation

    -- This module is DEPRECATED.
    import Data.AVL

    -- This module is DEPRECATED.
    import Data.AVL.Height

    -- This module is DEPRECATED.
    import Data.AVL.Indexed

    -- This module is DEPRECATED.
    import Data.AVL.Indexed.WithK

    -- This module is DEPRECATED.
    import Data.AVL.IndexedMap

    -- This module is DEPRECATED.
    import Data.AVL.Key

    -- This module is DEPRECATED.
    import Data.AVL.Map

    -- This module is DEPRECATED.
    import Data.AVL.NonEmpty

    -- This module is DEPRECATED.
    import Data.AVL.NonEmpty.Propositional

    -- This module is DEPRECATED.
    import Data.AVL.Sets

    -- This module is DEPRECATED.
    import Data.AVL.Value

    -- Booleans
    import Data.Bool

    -- The type for booleans and some operations
    import Data.Bool.Base

    -- Instances for booleans
    import Data.Bool.Instances

    -- Booleans: conjunction and disjunction of lists
    import Data.Bool.ListAction

    -- A bunch of properties
    import Data.Bool.Properties

    -- Showing booleans
    import Data.Bool.Show

    -- Automatic solvers for equations over booleans
    import Data.Bool.Solver

    -- Characters
    import Data.Char

    -- Basic definitions for Characters
    import Data.Char.Base

    -- Instances for characters
    import Data.Char.Instances

    -- Properties of operations on characters
    import Data.Char.Properties

    -- Containers, based on the work of Abbott and others
    import Data.Container

    -- This module is DEPRECATED. Please use
    -- Data.Container.Relation.Unary.Any directly.
    import Data.Container.Any

    -- Container combinators
    import Data.Container.Combinator

    -- Correctness proofs for container combinators
    import Data.Container.Combinator.Properties

    -- Fixpoints for containers - using guardedness
    import Data.Container.Fixpoints.Guarded

    -- The free monad construction on containers
    import Data.Container.FreeMonad

    -- Indexed containers aka interaction structures aka polynomial
    -- functors. The notation and presentation here is closest to that of
    -- Hancock and Hyvernat in "Programming interfaces and basic topology"
    -- (2006/9).
    import Data.Container.Indexed

    -- Indexed container combinators
    import Data.Container.Indexed.Combinator

    -- Greatest fixpoint for indexed containers - using guardedness
    import Data.Container.Indexed.Fixpoints.Guarded

    -- The free monad construction on indexed containers
    import Data.Container.Indexed.FreeMonad

    -- Equality over indexed container extensions parametrised by a setoid
    import Data.Container.Indexed.Relation.Binary.Equality.Setoid

    -- Pointwise equality for indexed containers
    import Data.Container.Indexed.Relation.Binary.Pointwise

    -- Properties of pointwise equality for indexed containers
    import Data.Container.Indexed.Relation.Binary.Pointwise.Properties

    -- Some code related to indexed containers that uses heterogeneous
    -- equality
    import Data.Container.Indexed.WithK

    -- Membership for containers
    import Data.Container.Membership

    -- Container Morphisms
    import Data.Container.Morphism

    -- Propertiers of any for containers
    import Data.Container.Morphism.Properties

    -- Properties of operations on containers
    import Data.Container.Properties

    -- Several kinds of "relatedness" for containers such as equivalences,
    -- surjections and bijections
    import Data.Container.Related

    -- Equality over container extensions parametrised by some setoid
    import Data.Container.Relation.Binary.Equality.Setoid

    -- Pointwise equality for containers
    import Data.Container.Relation.Binary.Pointwise

    -- Properties of pointwise equality for containers
    import Data.Container.Relation.Binary.Pointwise.Properties

    -- All (□) for containers
    import Data.Container.Relation.Unary.All

    -- Any (◇) for containers
    import Data.Container.Relation.Unary.Any

    -- Propertiers of any for containers
    import Data.Container.Relation.Unary.Any.Properties

    -- A way to specify that a function's argument takes a default value
    -- if the argument is not passed explicitly.
    import Data.Default

    -- Lists with fast append
    import Data.DifferenceList

    -- Natural numbers with fast addition (for use together with
    -- DifferenceVec)
    import Data.DifferenceNat

    -- Vectors with fast append
    import Data.DifferenceVec

    -- Digits and digit expansions
    import Data.Digit

    -- Properties of digits and digit expansions
    import Data.Digit.Properties

    -- Empty type, judgementally proof irrelevant, Level-monomorphic
    import Data.Empty

    -- An irrelevant version of ⊥-elim
    import Data.Empty.Irrelevant

    -- Level polymorphic Empty type
    import Data.Empty.Polymorphic

    -- This module is DEPRECATED.
    import Data.Erased

    -- Finite sets
    import Data.Fin

    -- Finite sets
    import Data.Fin.Base

    -- Induction over Fin
    import Data.Fin.Induction

    -- Instances for finite sets
    import Data.Fin.Instances

    -- Fin Literals
    import Data.Fin.Literals

    -- Patterns for Fin
    import Data.Fin.Patterns

    -- Bijections on finite sets (i.e. permutations).
    import Data.Fin.Permutation

    -- Component functions of permutations found in `Data.Fin.Permutation`
    import Data.Fin.Permutation.Components

    -- Decomposition of permutations into a list of transpositions.
    import Data.Fin.Permutation.Transposition.List

    -- Properties related to Fin, and operations making use of these
    -- properties (or other properties not available in Data.Fin)
    import Data.Fin.Properties

    -- Reflection utilities for Fin
    import Data.Fin.Reflection

    -- The 'top' view of Fin.
    import Data.Fin.Relation.Unary.Top

    -- Showing finite numbers
    import Data.Fin.Show

    -- Subsets of finite sets
    import Data.Fin.Subset

    -- Induction over Subset
    import Data.Fin.Subset.Induction

    -- Some properties about subsets
    import Data.Fin.Subset.Properties

    -- Substitutions
    import Data.Fin.Substitution

    -- This module is DEPRECATED. Please see
    -- `README.Data.Nat.Fin.Substitution.UntypedLambda` instead.
    import Data.Fin.Substitution.Example

    -- Substitution lemmas
    import Data.Fin.Substitution.Lemmas

    -- Application of substitutions to lists, along with various lemmas
    import Data.Fin.Substitution.List

    -- Floating point numbers
    import Data.Float

    -- Floats: basic types and operations
    import Data.Float.Base

    -- Instances for floating point numbers
    import Data.Float.Instances

    -- Properties of operations on floats
    import Data.Float.Properties

    -- Directed acyclic multigraphs
    import Data.Graph.Acyclic

    -- Integers
    import Data.Integer

    -- Integers, basic types and operations
    import Data.Integer.Base

    -- Coprimality
    import Data.Integer.Coprimality

    -- Integer division
    import Data.Integer.DivMod

    -- Unsigned divisibility
    import Data.Integer.Divisibility

    -- Alternative definition of divisibility without using modulus.
    import Data.Integer.Divisibility.Signed

    -- Greatest Common Divisor for integers
    import Data.Integer.GCD

    -- Instances for integers
    import Data.Integer.Instances

    -- Least Common Multiple for integers
    import Data.Integer.LCM

    -- Integer Literals
    import Data.Integer.Literals

    -- Some properties about integers
    import Data.Integer.Properties

    -- Some extra lemmas about natural numbers only needed for
    -- Data.Integer.Properties (for distributivity)
    import Data.Integer.Properties.NatLemmas

    -- Showing integers
    import Data.Integer.Show

    -- Automatic solvers for equations over integers
    import Data.Integer.Solver

    -- Automatic solvers for equations over integers
    import Data.Integer.Tactic.RingSolver

    -- Wrapper for the proof irrelevance modality
    import Data.Irrelevant

    -- Lists
    import Data.List

    -- Lists, basic types and operations
    import Data.List.Base

    -- This module is DEPRECATED. Please use
    -- `Data.List.Effectful` instead.
    import Data.List.Categorical

    -- This module is DEPRECATED. Please use
    -- `Data.List.Effectful.Transformer` instead.
    import Data.List.Categorical.Transformer

    -- A data structure which keeps track of an upper bound on the number
    -- of elements /not/ in a given list
    import Data.List.Countdown

    -- An effectful view of List
    import Data.List.Effectful

    -- List is Foldable
    import Data.List.Effectful.Foldable

    -- An effectful view of List
    import Data.List.Effectful.Transformer

    -- Finding the maximum/minimum values in a list
    import Data.List.Extrema

    -- Finding the maximum/minimum values in a list, specialised for Nat
    import Data.List.Extrema.Nat

    -- Fresh lists, a proof relevant variant of Catarina Coquand's contexts
    -- in "A Formalised Proof of the Soundness and Completeness of a Simply
    -- Typed Lambda-Calculus with Explicit Substitutions"
    import Data.List.Fresh

    -- Membership predicate for fresh lists
    import Data.List.Fresh.Membership.Setoid

    -- Properties of the membership predicate for fresh lists
    import Data.List.Fresh.Membership.Setoid.Properties

    -- A non-empty fresh list
    import Data.List.Fresh.NonEmpty

    -- Properties of fresh lists and functions acting on them
    import Data.List.Fresh.Properties

    -- All predicate transformer for fresh lists
    import Data.List.Fresh.Relation.Unary.All

    -- Properties of All predicate transformer for fresh lists
    import Data.List.Fresh.Relation.Unary.All.Properties

    -- Any predicate transformer for fresh lists
    import Data.List.Fresh.Relation.Unary.Any

    -- Properties of Any predicate transformer for fresh lists
    import Data.List.Fresh.Relation.Unary.Any.Properties

    -- Typeclass instances for List
    import Data.List.Instances

    -- An alternative definition of mutually-defined lists and non-empty
    -- lists, using the Kleene star and plus.
    import Data.List.Kleene

    -- A different interface to the Kleene lists, designed to mimic
    -- Data.List.
    import Data.List.Kleene.AsList

    -- Lists, based on the Kleene star and plus, basic types and operations.
    import Data.List.Kleene.Base

    -- List Literals
    import Data.List.Literals

    -- Decidable propositional membership over lists
    import Data.List.Membership.DecPropositional

    -- Decidable setoid membership over lists
    import Data.List.Membership.DecSetoid

    -- Data.List.Any.Membership instantiated with propositional equality,
    -- along with some additional definitions.
    import Data.List.Membership.Propositional

    -- Properties related to propositional list membership
    import Data.List.Membership.Propositional.Properties

    -- Properties related to propositional list membership, that rely on
    -- the K rule
    import Data.List.Membership.Propositional.Properties.WithK

    -- List membership and some related definitions
    import Data.List.Membership.Setoid

    -- Properties related to setoid list membership
    import Data.List.Membership.Setoid.Properties

    -- Nondependent N-ary functions manipulating lists
    import Data.List.Nary.NonDependent

    -- Non-empty lists
    import Data.List.NonEmpty

    -- Non-empty lists: base type and operations
    import Data.List.NonEmpty.Base

    -- This module is DEPRECATED. Please use
    -- `Data.List.NonEmpty.Effectful` instead.
    import Data.List.NonEmpty.Categorical

    -- This module is DEPRECATED. Please use
    -- `Data.List.NonEmpty.Effectful.Transformer` instead.
    import Data.List.NonEmpty.Categorical.Transformer

    -- An effectful view of List⁺
    import Data.List.NonEmpty.Effectful

    -- An effectful view of List
    import Data.List.NonEmpty.Effectful.Transformer

    -- Typeclass instances for List⁺
    import Data.List.NonEmpty.Instances

    -- Properties of non-empty lists
    import Data.List.NonEmpty.Properties

    -- Non-empty lists where all elements satisfy a given property
    import Data.List.NonEmpty.Relation.Unary.All

    -- List-related properties
    import Data.List.Properties

    -- Reflection utilities for List
    import Data.List.Reflection

    -- Bag and set equality
    import Data.List.Relation.Binary.BagAndSetEquality

    -- Decidability of the disjoint relation over propositional equality.
    import Data.List.Relation.Binary.Disjoint.DecPropositional

    -- Decidability of the disjoint relation over setoid equality.
    import Data.List.Relation.Binary.Disjoint.DecSetoid

    -- Pairs of lists that share no common elements (propositional equality)
    import Data.List.Relation.Binary.Disjoint.Propositional

    -- Properties of disjoint lists (propositional equality)
    import Data.List.Relation.Binary.Disjoint.Propositional.Properties

    -- Pairs of lists that share no common elements (setoid equality)
    import Data.List.Relation.Binary.Disjoint.Setoid

    -- Properties of disjoint lists (setoid equality)
    import Data.List.Relation.Binary.Disjoint.Setoid.Properties

    -- Decidable pointwise equality over lists using propositional equality
    import Data.List.Relation.Binary.Equality.DecPropositional

    -- Pointwise decidable equality over lists parameterised by a setoid
    import Data.List.Relation.Binary.Equality.DecSetoid

    -- Pointwise equality over lists using propositional equality
    import Data.List.Relation.Binary.Equality.Propositional

    -- Pointwise equality over lists parameterised by a setoid
    import Data.List.Relation.Binary.Equality.Setoid

    -- Properties of List modulo ≋
    import Data.List.Relation.Binary.Equality.Setoid.Properties

    -- An inductive definition of the heterogeneous infix relation
    import Data.List.Relation.Binary.Infix.Heterogeneous

    -- Properties of the heterogeneous infix relation
    import Data.List.Relation.Binary.Infix.Heterogeneous.Properties

    -- Properties of the homogeneous infix relation
    import Data.List.Relation.Binary.Infix.Homogeneous.Properties

    -- Lexicographic ordering of lists
    import Data.List.Relation.Binary.Lex

    -- Lexicographic ordering of lists
    import Data.List.Relation.Binary.Lex.NonStrict

    -- Lexicographic ordering of lists
    import Data.List.Relation.Binary.Lex.Strict

    -- A definition for the permutation relation using setoid equality
    import Data.List.Relation.Binary.Permutation.Homogeneous

    -- An inductive definition for the permutation relation
    import Data.List.Relation.Binary.Permutation.Propositional

    -- Properties of permutation
    import Data.List.Relation.Binary.Permutation.Propositional.Properties

    -- Properties of permutation (with K)
    import Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK

    -- A definition for the permutation relation using setoid equality
    import Data.List.Relation.Binary.Permutation.Setoid

    -- Properties of permutations using setoid equality
    import Data.List.Relation.Binary.Permutation.Setoid.Properties

    -- Properties of permutations using setoid equality (on Maybe elements)
    import Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe

    -- Pointwise lifting of relations to lists
    import Data.List.Relation.Binary.Pointwise

    -- Pointwise lifting of relations to lists
    import Data.List.Relation.Binary.Pointwise.Base

    -- Properties of pointwise lifting of relations to lists
    import Data.List.Relation.Binary.Pointwise.Properties

    -- An inductive definition of the heterogeneous prefix relation
    import Data.List.Relation.Binary.Prefix.Heterogeneous

    -- Properties of the heterogeneous prefix relation
    import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties

    -- Properties of the homogeneous prefix relation
    import Data.List.Relation.Binary.Prefix.Homogeneous.Properties

    -- Properties of the propositional prefix relation
    import Data.List.Relation.Binary.Prefix.Propositional.Properties

    -- An inductive definition of the sublist relation for types which have
    -- a decidable equality. This is commonly known as Order Preserving
    -- Embeddings (OPE).
    import Data.List.Relation.Binary.Sublist.DecPropositional

    -- A solver for proving that one list is a sublist of the other for
    -- types which enjoy decidable equalities.
    import Data.List.Relation.Binary.Sublist.DecPropositional.Solver

    -- An inductive definition of the sublist relation with respect to a
    -- setoid which is decidable. This is a generalisation of what is
    -- commonly known as Order Preserving Embeddings (OPE).
    import Data.List.Relation.Binary.Sublist.DecSetoid

    -- A solver for proving that one list is a sublist of the other.
    import Data.List.Relation.Binary.Sublist.DecSetoid.Solver

    -- An inductive definition of the heterogeneous sublist relation
    -- This is a generalisation of what is commonly known as Order
    -- Preserving Embeddings (OPE).
    import Data.List.Relation.Binary.Sublist.Heterogeneous

    -- Properties of the heterogeneous sublist relation
    import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties

    -- A solver for proving that one list is a sublist of the other.
    import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver

    -- An inductive definition of the sublist relation. This is commonly
    -- known as Order Preserving Embeddings (OPE).
    import Data.List.Relation.Binary.Sublist.Propositional

    -- This module is DEPRECATED.
    -- Please use `Data.List.Relation.Binary.Sublist.Propositional.Slice`
    -- instead.
    import Data.List.Relation.Binary.Sublist.Propositional.Disjoint

    -- A larger example for sublists (propositional case):
    -- Simply-typed lambda terms with globally unique variables
    -- (both bound and free ones).
    import Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables

    -- Sublist-related properties
    import Data.List.Relation.Binary.Sublist.Propositional.Properties

    -- Slices in the propositional sublist category.
    import Data.List.Relation.Binary.Sublist.Propositional.Slice

    -- An inductive definition of the sublist relation with respect to a
    -- setoid. This is a generalisation of what is commonly known as Order
    -- Preserving Embeddings (OPE).
    import Data.List.Relation.Binary.Sublist.Setoid

    -- Properties of the setoid sublist relation
    import Data.List.Relation.Binary.Sublist.Setoid.Properties

    -- Decidability of the subset relation over propositional equality.
    import Data.List.Relation.Binary.Subset.DecPropositional

    -- Decidability of the subset relation over setoid equality.
    import Data.List.Relation.Binary.Subset.DecSetoid

    -- The sublist relation over propositional equality.
    import Data.List.Relation.Binary.Subset.Propositional

    -- Properties of the sublist relation over setoid equality.
    import Data.List.Relation.Binary.Subset.Propositional.Properties

    -- The extensional sublist relation over setoid equality.
    import Data.List.Relation.Binary.Subset.Setoid

    -- Properties of the extensional sublist relation over setoid equality.
    import Data.List.Relation.Binary.Subset.Setoid.Properties

    -- An inductive definition of the heterogeneous suffix relation
    import Data.List.Relation.Binary.Suffix.Heterogeneous

    -- Properties of the heterogeneous suffix relation
    import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties

    -- Properties of the homogeneous suffix relation
    import Data.List.Relation.Binary.Suffix.Homogeneous.Properties

    -- Properties of the propositional suffix relation
    import Data.List.Relation.Binary.Suffix.Propositional.Properties

    -- Generalised view of appending two lists into one.
    import Data.List.Relation.Ternary.Appending

    -- Properties of the generalised view of appending two lists
    import Data.List.Relation.Ternary.Appending.Properties

    -- Appending of lists using propositional equality
    import Data.List.Relation.Ternary.Appending.Propositional

    -- Properties of list appending
    import Data.List.Relation.Ternary.Appending.Propositional.Properties

    -- Appending of lists using setoid equality
    import Data.List.Relation.Ternary.Appending.Setoid

    -- Properties of list appending
    import Data.List.Relation.Ternary.Appending.Setoid.Properties

    -- Generalised notion of interleaving two lists into one in an
    -- order-preserving manner
    import Data.List.Relation.Ternary.Interleaving

    -- Properties of general interleavings
    import Data.List.Relation.Ternary.Interleaving.Properties

    -- Interleavings of lists using propositional equality
    import Data.List.Relation.Ternary.Interleaving.Propositional

    -- Properties of interleaving using propositional equality
    import Data.List.Relation.Ternary.Interleaving.Propositional.Properties

    -- Interleavings of lists using setoid equality
    import Data.List.Relation.Ternary.Interleaving.Setoid

    -- Properties of interleaving using setoid equality
    import Data.List.Relation.Ternary.Interleaving.Setoid.Properties

    -- Lists where all elements satisfy a given property
    import Data.List.Relation.Unary.All

    -- Properties related to All
    import Data.List.Relation.Unary.All.Properties

    -- Lists where every pair of elements are related (symmetrically)
    import Data.List.Relation.Unary.AllPairs

    -- Properties related to AllPairs
    import Data.List.Relation.Unary.AllPairs.Properties

    -- Lists where at least one element satisfies a given property
    import Data.List.Relation.Unary.Any

    -- Properties related to Any
    import Data.List.Relation.Unary.Any.Properties

    -- Lists which contain every element of a given type
    import Data.List.Relation.Unary.Enumerates.Setoid

    -- Properties of lists which contain every element of a given type
    import Data.List.Relation.Unary.Enumerates.Setoid.Properties

    -- First generalizes the idea that an element is the first in a list to
    -- satisfy a predicate.
    import Data.List.Relation.Unary.First

    -- Properties of First
    import Data.List.Relation.Unary.First.Properties

    -- Property that elements are grouped
    import Data.List.Relation.Unary.Grouped

    -- Property related to Grouped
    import Data.List.Relation.Unary.Grouped.Properties

    -- Lists where every consecutative pair of elements is related.
    import Data.List.Relation.Unary.Linked

    -- Properties related to Linked
    import Data.List.Relation.Unary.Linked.Properties

    -- Sorted lists
    import Data.List.Relation.Unary.Sorted.TotalOrder

    -- Sorted lists
    import Data.List.Relation.Unary.Sorted.TotalOrder.Properties

    -- 'Sufficient' lists: a structurally inductive view of lists xs
    -- as given by xs ≡ non-empty prefix + sufficient suffix
    import Data.List.Relation.Unary.Sufficient

    -- Lists made up entirely of unique elements (setoid equality)
    import Data.List.Relation.Unary.Unique.DecPropositional

    -- Properties of lists made up entirely of decidably unique elements
    import Data.List.Relation.Unary.Unique.DecPropositional.Properties

    -- Lists made up entirely of unique elements (setoid equality)
    import Data.List.Relation.Unary.Unique.DecSetoid

    -- Properties of lists made up entirely of decidably unique elements
    import Data.List.Relation.Unary.Unique.DecSetoid.Properties

    -- Lists made up entirely of unique elements (propositional equality)
    import Data.List.Relation.Unary.Unique.Propositional

    -- Properties of unique lists (setoid equality)
    import Data.List.Relation.Unary.Unique.Propositional.Properties

    -- Lists made up entirely of unique elements (setoid equality)
    import Data.List.Relation.Unary.Unique.Setoid

    -- Properties of unique lists (setoid equality)
    import Data.List.Relation.Unary.Unique.Setoid.Properties

    -- Reverse view
    import Data.List.Reverse

    -- List scans: definitions
    import Data.List.Scans.Base

    -- List scans: properties
    import Data.List.Scans.Properties

    -- Showing lists
    import Data.List.Show

    -- This module is DEPRECATED.
    import Data.List.Solver

    -- Functions and definitions for sorting lists
    import Data.List.Sort

    -- The core definition of a sorting algorithm
    import Data.List.Sort.Base

    -- An implementation of insertion sort and its properties
    import Data.List.Sort.InsertionSort

    -- An implementation of insertion sort
    import Data.List.Sort.InsertionSort.Base

    -- Properties of insertion sort
    import Data.List.Sort.InsertionSort.Properties

    -- An implementation of merge sort along with proofs of correctness.
    import Data.List.Sort.MergeSort

    -- An implementation of merge sort
    import Data.List.Sort.MergeSort.Base

    -- An implementation of merge sort along with proofs of correctness.
    import Data.List.Sort.MergeSort.Properties

    -- List Zippers, basic types and operations
    import Data.List.Zipper

    -- List Zipper-related properties
    import Data.List.Zipper.Properties

    -- The Maybe type
    import Data.Maybe

    -- The Maybe type and some operations
    import Data.Maybe.Base

    -- This module is DEPRECATED. Please use
    -- `Data.Maybe.Effectful` instead.
    import Data.Maybe.Categorical

    -- This module is DEPRECATED. Please use
    -- `Data.Maybe.Effectful.Transformer` instead.
    import Data.Maybe.Categorical.Transformer

    -- An effectful view of Maybe
    import Data.Maybe.Effectful

    -- An effectful view of Maybe
    import Data.Maybe.Effectful.Transformer

    -- Typeclass instances for Maybe
    import Data.Maybe.Instances

    -- Maybe-related properties
    import Data.Maybe.Properties

    -- Lifting a relation such that `nothing` is also related to `just`
    import Data.Maybe.Relation.Binary.Connected

    -- Pointwise lifting of relations to maybes
    import Data.Maybe.Relation.Binary.Pointwise

    -- Maybes where all the elements satisfy a given property
    import Data.Maybe.Relation.Unary.All

    -- Properties related to All
    import Data.Maybe.Relation.Unary.All.Properties

    -- Maybes where one of the elements satisfies a given property
    import Data.Maybe.Relation.Unary.Any

    -- Natural numbers
    import Data.Nat

    -- Natural numbers, basic types and operations
    import Data.Nat.Base

    -- Natural numbers represented in binary natively in Agda.
    import Data.Nat.Binary

    -- Natural numbers represented in binary.
    import Data.Nat.Binary.Base

    -- Induction over _<_ for ℕᵇ.
    import Data.Nat.Binary.Induction

    -- Instances for binary natural numbers
    import Data.Nat.Binary.Instances

    -- Basic properties of ℕᵇ
    import Data.Nat.Binary.Properties

    -- Subtraction on Bin and some of its properties.
    import Data.Nat.Binary.Subtraction

    -- Combinatorial operations
    import Data.Nat.Combinatorics

    -- Combinatorics operations
    import Data.Nat.Combinatorics.Base

    -- The specification for combinatorics operations
    import Data.Nat.Combinatorics.Specification

    -- Coprimality
    import Data.Nat.Coprimality

    -- Natural number division
    import Data.Nat.DivMod

    -- More efficient mod and divMod operations (require the K axiom)
    import Data.Nat.DivMod.WithK

    -- Divisibility
    import Data.Nat.Divisibility

    -- Greatest common divisor
    import Data.Nat.GCD

    -- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
    import Data.Nat.GCD.Lemmas

    -- A generalisation of the arithmetic operations
    import Data.Nat.GeneralisedArithmetic

    -- Various forms of induction for natural numbers
    import Data.Nat.Induction

    -- Definition of and lemmas related to "true infinitely often"
    import Data.Nat.InfinitelyOften

    -- Instances for natural numbers
    import Data.Nat.Instances

    -- Least common multiple
    import Data.Nat.LCM

    -- Natural numbers: sum and product of lists
    import Data.Nat.ListAction

    -- Natural numbers: properties of sum and product
    import Data.Nat.ListAction.Properties

    -- Natural Literals
    import Data.Nat.Literals

    -- Logarithm base 2 and respective properties
    import Data.Nat.Logarithm

    -- Primality
    import Data.Nat.Primality

    -- Prime factorisation of natural numbers and its properties
    import Data.Nat.Primality.Factorisation

    -- A bunch of properties about natural number operations
    import Data.Nat.Properties

    -- Linear congruential pseudo random generators for natural numbers
    -- /!\ NB: LCGs must not be used for cryptographic applications
    import Data.Nat.PseudoRandom.LCG

    -- Reflection utilities for ℕ
    import Data.Nat.Reflection

    -- Showing natural numbers
    import Data.Nat.Show

    -- Properties of showing natural numbers
    import Data.Nat.Show.Properties

    -- Automatic solvers for equations over naturals
    import Data.Nat.Solver

    -- Automatic solvers for equations over naturals
    import Data.Nat.Tactic.RingSolver

    -- Natural number types and operations requiring the axiom K.
    import Data.Nat.WithK

    -- Parity
    import Data.Parity

    -- Parity
    import Data.Parity.Base

    -- Instances for parities
    import Data.Parity.Instances

    -- Some properties about parities
    import Data.Parity.Properties

    -- Products
    import Data.Product

    -- Algebraic properties of products
    import Data.Product.Algebra

    -- Products
    import Data.Product.Base

    -- This module is DEPRECATED. Please use
    -- `Data.Product.Categorical.Examples` instead.
    import Data.Product.Categorical.Examples

    -- This module is DEPRECATED. Please use
    -- `Data.Product.Categorical.Left` instead.
    import Data.Product.Categorical.Left

    -- This module is DEPRECATED. Please use
    -- `Data.Product.Categorical.Left.Base` instead.
    import Data.Product.Categorical.Left.Base

    -- This module is DEPRECATED. Please use
    -- `Data.Product.Categorical.Right` instead.
    import Data.Product.Categorical.Right

    -- This module is DEPRECATED. Please use
    -- `Data.Product.Categorical.Right.Base` instead.
    import Data.Product.Categorical.Right.Base

    -- Universe-sensitive functor and monad instances for the Product type.
    import Data.Product.Effectful.Examples

    -- Left-biased universe-sensitive functor and monad instances for the
    -- Product type.
    import Data.Product.Effectful.Left

    -- Base definitions for the left-biased universe-sensitive functor and
    -- monad instances for the Product type.
    import Data.Product.Effectful.Left.Base

    -- Right-biased universe-sensitive functor and monad instances for the
    -- Product type.
    import Data.Product.Effectful.Right

    -- Base definitions for the right-biased universe-sensitive functor
    -- and monad instances for the Product type.
    import Data.Product.Effectful.Right.Base

    -- Dependent product combinators for propositional equality
    -- preserving functions
    import Data.Product.Function.Dependent.Propositional

    -- Dependent product combinators for propositional equality
    -- preserving functions
    import Data.Product.Function.Dependent.Propositional.WithK

    -- Dependent product combinators for setoid equality preserving
    -- functions.
    import Data.Product.Function.Dependent.Setoid

    -- This module is DEPRECATED.
    import Data.Product.Function.Dependent.Setoid.WithK

    -- Non-dependent product combinators for propositional equality
    -- preserving functions
    import Data.Product.Function.NonDependent.Propositional

    -- Non-dependent product combinators for setoid equality preserving
    -- functions
    import Data.Product.Function.NonDependent.Setoid

    -- Typeclass instances for products
    import Data.Product.Instances

    -- Nondependent heterogeneous N-ary products
    import Data.Product.Nary.NonDependent

    -- Properties of products
    import Data.Product.Properties

    -- Properties of 'very dependent' map / zipWith over products
    import Data.Product.Properties.Dependent

    -- Properties, related to products, that rely on the K rule
    import Data.Product.Properties.WithK

    -- Lexicographic products of binary relations
    import Data.Product.Relation.Binary.Lex.NonStrict

    -- Lexicographic products of binary relations
    import Data.Product.Relation.Binary.Lex.Strict

    -- Pointwise lifting of binary relations to sigma types
    import Data.Product.Relation.Binary.Pointwise.Dependent

    -- Properties that are related to pointwise lifting of binary
    -- relations to sigma types and make use of heterogeneous equality
    import Data.Product.Relation.Binary.Pointwise.Dependent.WithK

    -- Pointwise products of binary relations
    import Data.Product.Relation.Binary.Pointwise.NonDependent

    -- Lifting of two predicates
    import Data.Product.Relation.Unary.All

    -- Rational numbers
    import Data.Rational

    -- Rational numbers
    import Data.Rational.Base

    -- Instances for rational numbers
    import Data.Rational.Instances

    -- Rational Literals
    import Data.Rational.Literals

    -- Properties of Rational numbers
    import Data.Rational.Properties

    -- Showing rational numbers
    import Data.Rational.Show

    -- Automatic solvers for equations over rationals
    import Data.Rational.Solver

    -- Rational numbers in non-reduced form.
    import Data.Rational.Unnormalised

    -- Rational numbers in non-reduced form.
    import Data.Rational.Unnormalised.Base

    -- Properties of unnormalized Rational numbers
    import Data.Rational.Unnormalised.Properties

    -- Showing unnormalised rational numbers
    import Data.Rational.Unnormalised.Show

    -- Automatic solvers for equations over rationals
    import Data.Rational.Unnormalised.Solver

    -- Record types with manifest fields and "with", based on Randy
    -- Pollack's "Dependently Typed Records in Type Theory"
    import Data.Record

    -- Refinement type: a value together with a proof irrelevant witness.
    import Data.Refinement

    -- Refinement type: a value together with a proof irrelevant witness.
    import Data.Refinement.Base

    -- Properties of refinement types
    import Data.Refinement.Properties

    -- Predicate lifting for refinement types
    import Data.Refinement.Relation.Unary.All

    -- Signs
    import Data.Sign

    -- Signs
    import Data.Sign.Base

    -- Instances for signs
    import Data.Sign.Instances

    -- Some properties about signs
    import Data.Sign.Properties

    -- Showing signs
    import Data.Sign.Show

    -- Bounded vectors (inefficient implementation)
    import Data.Star.BoundedVec

    -- Decorated star-lists
    import Data.Star.Decoration

    -- Environments (heterogeneous collections)
    import Data.Star.Environment

    -- Finite sets defined using the reflexive-transitive closure, Star
    import Data.Star.Fin

    -- Lists defined in terms of the reflexive-transitive closure, Star
    import Data.Star.List

    -- Natural numbers defined using the reflexive-transitive closure, Star
    import Data.Star.Nat

    -- Pointers into star-lists
    import Data.Star.Pointer

    -- Vectors defined in terms of the reflexive-transitive closure, Star
    import Data.Star.Vec

    -- Strings
    import Data.String

    -- Strings: builtin type and basic operations
    import Data.String.Base

    -- Instances for strings
    import Data.String.Instances

    -- String Literals
    import Data.String.Literals

    -- Properties of operations on strings
    import Data.String.Properties

    -- Sums (disjoint unions)
    import Data.Sum

    -- Algebraic properties of sums (disjoint unions)
    import Data.Sum.Algebra

    -- Sums (disjoint unions)
    import Data.Sum.Base

    -- This module is DEPRECATED. Please use
    -- `Data.Sum.Categorical.Examples` instead.
    import Data.Sum.Categorical.Examples

    -- This module is DEPRECATED. Please use
    -- `Data.Sum.Categorical.Left` instead.
    import Data.Sum.Categorical.Left

    -- This module is DEPRECATED. Please use
    -- `Data.Sum.Categorical.Left.Transformer` instead.
    import Data.Sum.Categorical.Left.Transformer

    -- This module is DEPRECATED. Please use
    -- `Data.Sum.Categorical.Right` instead.
    import Data.Sum.Categorical.Right

    -- This module is DEPRECATED. Please use
    -- `Data.Sum.Categorical.Right.Transformer` instead.
    import Data.Sum.Categorical.Right.Transformer

    -- Usage examples of the effectful view of the Sum type
    import Data.Sum.Effectful.Examples

    -- An effectful view of the Sum type (Left-biased)
    import Data.Sum.Effectful.Left

    -- An effectful view of the Sum type (Left-biased)
    import Data.Sum.Effectful.Left.Transformer

    -- An effectful view of the Sum type (Right-biased)
    import Data.Sum.Effectful.Right

    -- An effectful view of the Sum type (Right-biased)
    import Data.Sum.Effectful.Right.Transformer

    -- Sum combinators for propositional equality preserving functions
    import Data.Sum.Function.Propositional

    -- Sum combinators for setoid equality preserving functions
    import Data.Sum.Function.Setoid

    -- Typeclass instances for sums
    import Data.Sum.Instances

    -- Properties of sums (disjoint unions)
    import Data.Sum.Properties

    -- Sums of binary relations
    import Data.Sum.Relation.Binary.LeftOrder

    -- Pointwise sum
    import Data.Sum.Relation.Binary.Pointwise

    -- Heterogeneous `All` predicate for disjoint sums
    import Data.Sum.Relation.Unary.All

    -- An either-or-both data type
    import Data.These

    -- An either-or-both data type, basic type and operations
    import Data.These.Base

    -- This module is DEPRECATED. Please use
    -- `Data.These.Categorical.Left` instead.
    import Data.These.Categorical.Left

    -- This module is DEPRECATED. Please use
    -- `Data.These.Categorical.Left.Base` instead.
    import Data.These.Categorical.Left.Base

    -- This module is DEPRECATED. Please use
    -- `Data.These.Categorical.Right` instead.
    import Data.These.Categorical.Right

    -- This module is DEPRECATED. Please use
    -- `Data.These.Categorical.Right.Base` instead.
    import Data.These.Categorical.Right.Base

    -- Left-biased universe-sensitive functor and monad instances for These.
    import Data.These.Effectful.Left

    -- Base definitions for the left-biased universe-sensitive functor and
    -- monad instances for These.
    import Data.These.Effectful.Left.Base

    -- Right-biased universe-sensitive functor and monad instances for These.
    import Data.These.Effectful.Right

    -- Base definitions for the right-biased universe-sensitive functor and
    -- monad instances for These.
    import Data.These.Effectful.Right.Base

    -- Typeclass instances for These
    import Data.These.Instances

    -- Properties of These
    import Data.These.Properties

    -- AVL trees
    import Data.Tree.AVL

    -- Types and functions which are used to keep track of height
    -- invariants in AVL Trees
    import Data.Tree.AVL.Height

    -- AVL trees where the stored values may depend on their key
    import Data.Tree.AVL.Indexed

    -- AVL trees whose elements satisfy a given property
    import Data.Tree.AVL.Indexed.Relation.Unary.All

    -- AVL trees where at least one element satisfies a given property
    import Data.Tree.AVL.Indexed.Relation.Unary.Any

    -- Properties related to Any
    import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties

    -- Some code related to indexed AVL trees that relies on the K rule
    import Data.Tree.AVL.Indexed.WithK

    -- Finite maps with indexed keys and values, based on AVL trees
    import Data.Tree.AVL.IndexedMap

    -- Keys for AVL trees -- the original key type extended with a new
    -- minimum and maximum.
    import Data.Tree.AVL.Key

    -- Maps from keys to values, based on AVL trees
    -- This modules provides a simpler map interface, without a dependency
    -- between the key and value types.
    import Data.Tree.AVL.Map

    -- Membership relation for AVL Maps identifying values up to
    -- propositional equality.
    import Data.Tree.AVL.Map.Membership.Propositional

    -- Properties of the membership relation for AVL Maps identifying values
    -- up to propositional equality.
    import Data.Tree.AVL.Map.Membership.Propositional.Properties

    -- AVL trees where at least one element satisfies a given property
    import Data.Tree.AVL.Map.Relation.Unary.Any

    -- Non-empty AVL trees
    import Data.Tree.AVL.NonEmpty

    -- Non-empty AVL trees, where equality for keys is propositional equality
    import Data.Tree.AVL.NonEmpty.Propositional

    -- AVL trees where at least one element satisfies a given property
    import Data.Tree.AVL.Relation.Unary.Any

    -- Finite sets, based on AVL trees
    import Data.Tree.AVL.Sets

    -- Membership relation for AVL sets
    import Data.Tree.AVL.Sets.Membership

    -- Properties of membership for AVL sets
    import Data.Tree.AVL.Sets.Membership.Properties

    -- Values for AVL trees
    -- Values must respect the underlying equivalence on keys
    import Data.Tree.AVL.Value

    -- Binary Trees
    import Data.Tree.Binary

    -- Properties of binary trees
    import Data.Tree.Binary.Properties

    -- Pointwise lifting of a predicate to a binary tree
    import Data.Tree.Binary.Relation.Unary.All

    -- Properties of the pointwise lifting of a predicate to a binary tree
    import Data.Tree.Binary.Relation.Unary.All.Properties

    -- Zippers for Binary Trees
    import Data.Tree.Binary.Zipper

    -- Tree Zipper-related properties
    import Data.Tree.Binary.Zipper.Properties

    -- The unit type, Level-monomorphic version
    import Data.Unit

    -- The unit type and the total relation on unit
    import Data.Unit.Base

    -- Instances for the unit type
    import Data.Unit.Instances

    -- Some unit types
    import Data.Unit.NonEta

    -- The universe polymorphic unit type and the total relation on unit
    import Data.Unit.Polymorphic

    -- A universe polymorphic unit type, as a Lift of the Level 0 one.
    import Data.Unit.Polymorphic.Base

    -- Instances for the polymorphic unit type
    import Data.Unit.Polymorphic.Instances

    -- Properties of the polymorphic unit type
    -- Defines Decidable Equality and Decidable Ordering as well
    import Data.Unit.Polymorphic.Properties

    -- Properties of the unit type
    import Data.Unit.Properties

    -- Universes
    import Data.Universe

    -- Indexed universes
    import Data.Universe.Indexed

    -- Vectors
    import Data.Vec

    -- Vectors, basic types and operations
    import Data.Vec.Base

    -- Bounded vectors
    import Data.Vec.Bounded

    -- Bounded vectors, basic types and operations
    import Data.Vec.Bounded.Base

    -- Showing bounded vectors
    import Data.Vec.Bounded.Show

    -- This module is DEPRECATED. Please use
    -- `Data.Vec.Effectful` instead.
    import Data.Vec.Categorical

    -- This module is DEPRECATED. Please use
    -- `Data.Vec.Effectful.Transformer` instead.
    import Data.Vec.Categorical.Transformer

    -- An effectful view of Vec
    import Data.Vec.Effectful

    -- Vec is Foldable
    import Data.Vec.Effectful.Foldable

    -- An effectful view of Vec
    import Data.Vec.Effectful.Transformer

    -- Vectors defined as functions from a finite set to a type.
    import Data.Vec.Functional

    -- Some Vector-related properties
    import Data.Vec.Functional.Properties

    -- Pointwise lifting of relations over Vector
    import Data.Vec.Functional.Relation.Binary.Equality.Setoid

    -- Permutation relations over Vector
    import Data.Vec.Functional.Relation.Binary.Permutation

    -- Properties of permutation
    import Data.Vec.Functional.Relation.Binary.Permutation.Properties

    -- Pointwise lifting of relations over Vector
    import Data.Vec.Functional.Relation.Binary.Pointwise

    -- Properties related to Pointwise
    import Data.Vec.Functional.Relation.Binary.Pointwise.Properties

    -- Universal lifting of predicates over Vectors
    import Data.Vec.Functional.Relation.Unary.All

    -- Properties related to All
    import Data.Vec.Functional.Relation.Unary.All.Properties

    -- Existential lifting of predicates over Vectors
    import Data.Vec.Functional.Relation.Unary.Any

    -- Typeclass instances for Vec
    import Data.Vec.Instances

    -- Decidable propositional membership over vectors
    import Data.Vec.Membership.DecPropositional

    -- Decidable setoid membership over vectors.
    import Data.Vec.Membership.DecSetoid

    -- Data.Vec.Any.Membership instantiated with propositional equality,
    -- along with some additional definitions.
    import Data.Vec.Membership.Propositional

    -- Properties of membership of vectors based on propositional equality.
    import Data.Vec.Membership.Propositional.Properties

    -- Membership of vectors, along with some additional definitions.
    import Data.Vec.Membership.Setoid

    -- Code for converting Vec A n → B to and from n-ary functions
    import Data.Vec.N-ary

    -- Some Vec-related properties
    import Data.Vec.Properties

    -- Some Vec-related properties that depend on the K rule or make use
    -- of heterogeneous equality
    import Data.Vec.Properties.WithK

    -- Vectors defined by recursion
    import Data.Vec.Recursive

    -- This module is DEPRECATED. Please use
    -- `Data.Vec.Recursive.Effectful` instead.
    import Data.Vec.Recursive.Categorical

    -- An effectful view of vectors defined by recursion
    import Data.Vec.Recursive.Effectful

    -- Properties of n-ary products
    import Data.Vec.Recursive.Properties

    -- Reflection utilities for Vector
    import Data.Vec.Reflection

    -- An equational reasoning library for propositional equality over
    -- vectors of different indices using cast.
    import Data.Vec.Relation.Binary.Equality.Cast

    -- Decidable vector equality over propositional equality
    import Data.Vec.Relation.Binary.Equality.DecPropositional

    -- Decidable semi-heterogeneous vector equality over setoids
    import Data.Vec.Relation.Binary.Equality.DecSetoid

    -- Vector equality over propositional equality
    import Data.Vec.Relation.Binary.Equality.Propositional

    -- Code related to vector equality over propositional equality that
    -- makes use of heterogeneous equality
    import Data.Vec.Relation.Binary.Equality.Propositional.WithK

    -- Semi-heterogeneous vector equality over setoids
    import Data.Vec.Relation.Binary.Equality.Setoid

    -- Lexicographic ordering of same-length vector
    import Data.Vec.Relation.Binary.Lex.NonStrict

    -- Lexicographic ordering of lists of same-length vectors
    import Data.Vec.Relation.Binary.Lex.Strict

    -- Extensional pointwise lifting of relations to vectors
    import Data.Vec.Relation.Binary.Pointwise.Extensional

    -- Inductive pointwise lifting of relations to vectors
    import Data.Vec.Relation.Binary.Pointwise.Inductive

    -- Vectors where all elements satisfy a given property
    import Data.Vec.Relation.Unary.All

    -- Properties related to All
    import Data.Vec.Relation.Unary.All.Properties

    -- Vectors where every pair of elements are related (symmetrically)
    import Data.Vec.Relation.Unary.AllPairs

    -- Properties related to AllPairs
    import Data.Vec.Relation.Unary.AllPairs.Properties

    -- Vectors where at least one element satisfies a given property
    import Data.Vec.Relation.Unary.Any

    -- Properties of vector's Any
    import Data.Vec.Relation.Unary.Any.Properties

    -- Vectors where every consecutative pair of elements is related.
    import Data.Vec.Relation.Unary.Linked

    -- Properties related to Linked
    import Data.Vec.Relation.Unary.Linked.Properties

    -- Vectors made up entirely of unique elements (propositional equality)
    import Data.Vec.Relation.Unary.Unique.Propositional

    -- Properties of unique vectors (setoid equality)
    import Data.Vec.Relation.Unary.Unique.Propositional.Properties

    -- Vectors made up entirely of unique elements (setoid equality)
    import Data.Vec.Relation.Unary.Unique.Setoid

    -- Properties of unique vectors (setoid equality)
    import Data.Vec.Relation.Unary.Unique.Setoid.Properties

    -- Showing vectors
    import Data.Vec.Show

    -- W-types
    import Data.W

    -- Indexed W-types aka Petersson-Synek trees
    import Data.W.Indexed

    -- Some code related to the W type that relies on the K rule
    import Data.W.WithK

    -- This module is DEPRECATED. Please use Data.Word64 instead
    import Data.Word

    -- This module is DEPRECATED. Please use Data.Word64.Base instead
    import Data.Word.Base

    -- This module is DEPRECATED. Please use Data.Word64.Instances instead
    import Data.Word.Instances

    -- This module is DEPRECATED. Please use Data.Word64.Properties instead
    import Data.Word.Properties

    -- Machine words
    import Data.Word64

    -- Machine words: basic type and conversion functions
    import Data.Word64.Base

    -- Instances for words
    import Data.Word64.Instances

    -- Word64 Literals
    import Data.Word64.Literals

    -- Properties of operations on machine words
    import Data.Word64.Properties

    -- Turn a relation into a record definition so as to remember the things
    -- being related.
    -- This module has a readme file: README.Data.Wrap
    import Data.Wrap

    -- Applicative functors
    import Effect.Applicative

    -- Indexed applicative functors
    import Effect.Applicative.Indexed

    -- Applicative functors on indexed sets (predicates)
    import Effect.Applicative.Predicate

    -- Type constructors giving rise to a semigroup at every type
    -- e.g. (List, _++_)
    import Effect.Choice

    -- Comonads
    import Effect.Comonad

    -- Empty values (e.g. [] for List, nothing for Maybe)
    import Effect.Empty

    -- Foldable functors
    import Effect.Foldable

    -- Functors
    import Effect.Functor

    -- Functors on indexed sets (predicates)
    import Effect.Functor.Predicate

    -- Monads
    import Effect.Monad

    -- A delimited continuation monad
    import Effect.Monad.Continuation

    -- The error monad transformer
    import Effect.Monad.Error.Transformer

    -- An effectful view of the identity function
    import Effect.Monad.Identity

    -- Typeclass instances for Identity
    import Effect.Monad.Identity.Instances

    -- Indexed monads
    import Effect.Monad.Indexed

    -- The partiality monad
    import Effect.Monad.Partiality

    -- An All predicate for the partiality monad
    import Effect.Monad.Partiality.All

    -- Typeclass instances for _⊥
    import Effect.Monad.Partiality.Instances

    -- Monads on indexed sets (predicates)
    import Effect.Monad.Predicate

    -- The reader monad
    import Effect.Monad.Reader

    -- The indexed reader monad
    import Effect.Monad.Reader.Indexed

    -- Instances for the reader monad
    import Effect.Monad.Reader.Instances

    -- The reader monad transformer
    import Effect.Monad.Reader.Transformer

    -- Basic type and definition of the reader monad transformer
    import Effect.Monad.Reader.Transformer.Base

    -- The state monad
    import Effect.Monad.State

    -- The indexed state monad
    import Effect.Monad.State.Indexed

    -- Instances for the state monad
    import Effect.Monad.State.Instances

    -- The state monad transformer
    import Effect.Monad.State.Transformer

    -- Basic definition and functions on the state monad transformer
    import Effect.Monad.State.Transformer.Base

    -- The writer monad
    import Effect.Monad.Writer

    -- The indexed writer monad
    import Effect.Monad.Writer.Indexed

    -- Instances for the writer monad
    import Effect.Monad.Writer.Instances

    -- The writer monad transformer
    import Effect.Monad.Writer.Transformer

    -- Basic type and definition of the writer monad transformer
    import Effect.Monad.Writer.Transformer.Base

    -- Functions
    import Function

    -- Simple combinators working solely on and with functions
    import Function.Base

    -- This module is DEPRECATED.
    import Function.Bijection

    -- Bundles for types of functions
    import Function.Bundles

    -- Relationships between properties of functions. See
    -- `Function.Consequences.Propositional` for specialisations to
    -- propositional equality.
    import Function.Consequences

    -- Relationships between properties of functions where the equality
    -- over both the domain and codomain is assumed to be _≡_
    import Function.Consequences.Propositional

    -- Relationships between properties of functions where the equality
    -- over both the domain and codomain are assumed to be setoids.
    import Function.Consequences.Setoid

    -- Composition of functional properties
    import Function.Construct.Composition

    -- The constant function
    import Function.Construct.Constant

    -- The identity function
    import Function.Construct.Identity

    -- Some functional properties are symmetric
    import Function.Construct.Symmetry

    -- Definitions for types of functions.
    import Function.Definitions

    -- Bundles for types of functions
    import Function.Dependent.Bundles

    -- Endomorphisms on a Set
    import Function.Endo.Propositional

    -- Endomorphisms on a Setoid
    import Function.Endo.Setoid

    -- This module is DEPRECATED.
    import Function.Endomorphism.Propositional

    -- This module is DEPRECATED.
    import Function.Endomorphism.Setoid

    -- This module is DEPRECATED.
    import Function.Equality

    -- This module is DEPRECATED.
    import Function.Equivalence

    -- This module is DEPRECATED.
    import Function.HalfAdjointEquivalence

    -- This module is DEPRECATED. Please use
    -- `Function.Identity.Effectful` instead.
    import Function.Identity.Categorical

    -- An effectful view of the identity function
    import Function.Identity.Effectful

    -- Operations on Relations for Indexed sets
    import Function.Indexed.Bundles

    -- Function setoids and related constructions
    import Function.Indexed.Relation.Binary.Equality

    -- This module is DEPRECATED.
    import Function.Injection

    -- This module is DEPRECATED.
    import Function.Inverse

    -- This module is DEPRECATED.
    import Function.LeftInverse

    -- Metrics with arbitrary domains and codomains
    import Function.Metric

    -- Bundles for metrics
    import Function.Metric.Bundles

    -- Definitions of properties over distance functions
    import Function.Metric.Definitions

    -- Metrics with ℕ as the codomain of the metric function
    import Function.Metric.Nat

    -- Bundles for metrics over ℕ
    import Function.Metric.Nat.Bundles

    -- Core definitions for metrics over ℕ
    import Function.Metric.Nat.Definitions

    -- Core definitions for metrics over ℕ
    import Function.Metric.Nat.Structures

    -- Metrics with ℚ as the codomain of the metric function
    import Function.Metric.Rational

    -- Bundles for metrics over ℚ
    import Function.Metric.Rational.Bundles

    -- Core definitions for metrics over ℚ
    import Function.Metric.Rational.Definitions

    -- Core definitions for metrics over ℚ
    import Function.Metric.Rational.Structures

    -- Some metric structures (not packed up with sets, operations, etc.)
    import Function.Metric.Structures

    -- Heterogeneous N-ary Functions
    import Function.Nary.NonDependent

    -- Heterogeneous N-ary Functions: basic types and operations
    import Function.Nary.NonDependent.Base

    -- Basic properties of the function type
    import Function.Properties

    -- Some basic properties of bijections.
    import Function.Properties.Bijection

    -- Some basic properties of equivalences. This file is designed to be
    -- imported qualified.
    import Function.Properties.Equivalence

    -- Properties for injections
    import Function.Properties.Injection

    -- Properties of inverses.
    import Function.Properties.Inverse

    -- Half adjoint equivalences
    import Function.Properties.Inverse.HalfAdjointEquivalence

    -- Properties of right inverses
    import Function.Properties.RightInverse

    -- Properties of surjections
    import Function.Properties.Surjection

    -- A module used for creating function pipelines, see
    -- README.Function.Reasoning for examples
    import Function.Reasoning

    -- This module is DEPRECATED.
    import Function.Related

    -- Relatedness for the function hierarchy
    import Function.Related.Propositional

    -- Basic lemmas showing that various types are related (isomorphic or
    -- equivalent or…)
    import Function.Related.TypeIsomorphisms

    -- Automatic solver for equations over product and sum types
    import Function.Related.TypeIsomorphisms.Solver

    -- Function Equality setoid
    import Function.Relation.Binary.Setoid.Equality

    -- Strict combinators (i.e. that use call-by-value)
    import Function.Strict

    -- Structures for types of functions
    import Function.Structures

    -- Ways to give instances of certain structures where some fields can
    -- be given in terms of others.
    -- The contents of this file should usually be accessed from `Function`.
    import Function.Structures.Biased

    -- This module is DEPRECATED.
    import Function.Surjection

    -- An abstraction of various forms of recursion/induction
    import Induction

    -- A standard consequence of accessibility/well-foundedness:
    -- the impossibility of 'infinite descent' from any (accessible)
    -- element x satisfying P to 'smaller' y also satisfying P
    import Induction.InfiniteDescent

    -- Lexicographic induction
    import Induction.Lexicographic

    -- Well-founded induction
    import Induction.WellFounded

    -- Universe levels
    import Level

    -- Conversion from naturals to universe levels
    import Level.Literals

    -- Support for reflection
    import Reflection

    -- The reflected abstract syntax tree
    import Reflection.AST

    -- Abstractions used in the reflection machinery
    import Reflection.AST.Abstraction

    -- Alpha equality over terms
    import Reflection.AST.AlphaEquality

    -- Arguments used in the reflection machinery
    import Reflection.AST.Argument

    -- Argument information used in the reflection machinery
    import Reflection.AST.Argument.Information

    -- Modalities used in the reflection machinery
    import Reflection.AST.Argument.Modality

    -- Argument quantities used in the reflection machinery
    import Reflection.AST.Argument.Quantity

    -- Argument relevance used in the reflection machinery
    import Reflection.AST.Argument.Relevance

    -- Argument visibility used in the reflection machinery
    import Reflection.AST.Argument.Visibility

    -- Weakening, strengthening and free variable check for reflected terms.
    import Reflection.AST.DeBruijn

    -- Definitions used in the reflection machinery
    import Reflection.AST.Definition

    -- Instances for reflected syntax
    import Reflection.AST.Instances

    -- Literals used in the reflection machinery
    import Reflection.AST.Literal

    -- Metavariables used in the reflection machinery
    import Reflection.AST.Meta

    -- Names used in the reflection machinery
    import Reflection.AST.Name

    -- Patterns used in the reflection machinery
    import Reflection.AST.Pattern

    -- Converting reflection machinery to strings
    import Reflection.AST.Show

    -- Terms used in the reflection machinery
    import Reflection.AST.Term

    -- de Bruijn-aware generic traversal of reflected terms.
    import Reflection.AST.Traversal

    -- A universe for the types involved in the reflected syntax.
    import Reflection.AST.Universe

    -- Annotated reflected syntax.
    import Reflection.AnnotatedAST

    -- Computing free variable annotations on reflected syntax.
    import Reflection.AnnotatedAST.Free

    -- Support for system calls as part of reflection
    import Reflection.External

    -- The TC (Type Checking) monad
    import Reflection.TCM

    -- This module is DEPRECATED. Please use
    -- `Reflection.TCM.Effectful` instead.
    import Reflection.TCM.Categorical

    -- Typeclass instances for TC
    import Reflection.TCM.Effectful

    -- Printf-style versions of typeError and debugPrint
    import Reflection.TCM.Format

    -- Typeclass instances for TC
    import Reflection.TCM.Instances

    -- Monad syntax for the TC monad
    import Reflection.TCM.Syntax

    -- Reflection utilities
    import Reflection.TCM.Utilities

    -- Properties of homogeneous binary relations
    import Relation.Binary

    -- Bundles for homogeneous binary relations
    import Relation.Binary.Bundles

    -- Raw bundles for homogeneous binary relations
    import Relation.Binary.Bundles.Raw

    -- Some properties imply others
    import Relation.Binary.Consequences

    -- A pointwise lifting of a relation to incorporate new extrema.
    import Relation.Binary.Construct.Add.Extrema.Equality

    -- The lifting of a non-strict order to incorporate new extrema
    import Relation.Binary.Construct.Add.Extrema.NonStrict

    -- The lifting of a strict order to incorporate new extrema
    import Relation.Binary.Construct.Add.Extrema.Strict

    -- A pointwise lifting of a relation to incorporate a new infimum.
    import Relation.Binary.Construct.Add.Infimum.Equality

    -- The lifting of a non-strict order to incorporate a new infimum
    import Relation.Binary.Construct.Add.Infimum.NonStrict

    -- The lifting of a strict order to incorporate a new infimum
    import Relation.Binary.Construct.Add.Infimum.Strict

    -- A pointwise lifting of a relation to incorporate an additional point.
    import Relation.Binary.Construct.Add.Point.Equality

    -- A pointwise lifting of a relation to incorporate a new supremum.
    import Relation.Binary.Construct.Add.Supremum.Equality

    -- The lifting of a non-strict order to incorporate a new supremum
    import Relation.Binary.Construct.Add.Supremum.NonStrict

    -- The lifting of a strict order to incorporate a new supremum
    import Relation.Binary.Construct.Add.Supremum.Strict

    -- The universal binary relation
    import Relation.Binary.Construct.Always

    -- The reflexive, symmetric and transitive closure of a binary
    -- relation (aka the equivalence closure).
    import Relation.Binary.Construct.Closure.Equivalence

    -- Some properties of equivalence closures.
    import Relation.Binary.Construct.Closure.Equivalence.Properties

    -- Reflexive closures
    import Relation.Binary.Construct.Closure.Reflexive

    -- Some properties of reflexive closures
    import Relation.Binary.Construct.Closure.Reflexive.Properties

    -- Some properties of reflexive closures which rely on the K rule
    import Relation.Binary.Construct.Closure.Reflexive.Properties.WithK

    -- The reflexive transitive closures of McBride, Norell and Jansson
    import Relation.Binary.Construct.Closure.ReflexiveTransitive

    -- Some properties of reflexive transitive closures.
    import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties

    -- Properties, related to reflexive transitive closures, that rely on
    -- the K rule
    import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK

    -- Symmetric closures of binary relations
    import Relation.Binary.Construct.Closure.Symmetric

    -- Symmetric transitive closures of binary relations
    import Relation.Binary.Construct.Closure.SymmetricTransitive

    -- Transitive closures
    import Relation.Binary.Construct.Closure.Transitive

    -- Some code related to transitive closures that relies on the K rule
    import Relation.Binary.Construct.Closure.Transitive.WithK

    -- Composition of two binary relations
    import Relation.Binary.Construct.Composition

    -- The binary relation defined by a constant
    import Relation.Binary.Construct.Constant

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Construct.Flip.EqAndOrd` instead.
    import Relation.Binary.Construct.Converse

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Construct.Flip.Ord` instead.
    import Relation.Binary.Construct.Flip

    -- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
    -- the module `Relation.Binary.Construct.Flip.Ord` this module does not
    -- flip the underlying equality.
    import Relation.Binary.Construct.Flip.EqAndOrd

    -- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
    -- the module `Relation.Binary.Construct.Flip.EqAndOrd` this module
    -- flips both the relation and the underlying equality.
    import Relation.Binary.Construct.Flip.Ord

    -- Every respectful unary relation induces a preorder. No claim is
    -- made that this preorder is unique.
    import Relation.Binary.Construct.FromPred

    -- Every respectful binary relation induces a preorder. No claim is
    -- made that this preorder is unique.
    import Relation.Binary.Construct.FromRel

    -- Symmetric interior of a binary relation
    import Relation.Binary.Construct.Interior.Symmetric

    -- Intersection of two binary relations
    import Relation.Binary.Construct.Intersection

    -- Conversion of binary operators to binary relations via the left
    -- natural order.
    import Relation.Binary.Construct.NaturalOrder.Left

    -- Conversion of binary operators to binary relations via the right
    -- natural order.
    import Relation.Binary.Construct.NaturalOrder.Right

    -- The empty binary relation
    import Relation.Binary.Construct.Never

    -- Conversion of _≤_ to _<_
    import Relation.Binary.Construct.NonStrictToStrict

    -- Many properties which hold for `_∼_` also hold for `_∼_ on f`
    import Relation.Binary.Construct.On

    -- Conversion of < to ≤, along with a number of properties
    import Relation.Binary.Construct.StrictToNonStrict

    -- Substituting equalities for binary relations
    import Relation.Binary.Construct.Subst.Equality

    -- Union of two binary relations
    import Relation.Binary.Construct.Union

    -- Properties of binary relations
    import Relation.Binary.Definitions

    -- Heterogeneous equality
    import Relation.Binary.HeterogeneousEquality

    -- Quotients for Heterogeneous equality
    import Relation.Binary.HeterogeneousEquality.Quotients

    -- Example of a Quotient: ℤ as (ℕ × ℕ / ∼)
    import Relation.Binary.HeterogeneousEquality.Quotients.Examples

    -- Heterogeneously-indexed binary relations
    import Relation.Binary.Indexed.Heterogeneous

    -- Indexed binary relations
    import Relation.Binary.Indexed.Heterogeneous.Bundles

    -- Instantiates indexed binary structures at an index to the equivalent
    -- non-indexed structures.
    import Relation.Binary.Indexed.Heterogeneous.Construct.At

    -- Creates trivially indexed records from their non-indexed counterpart.
    import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial

    -- Indexed binary relations
    import Relation.Binary.Indexed.Heterogeneous.Definitions

    -- Indexed binary relations
    import Relation.Binary.Indexed.Heterogeneous.Structures

    -- Homogeneously-indexed binary relations
    import Relation.Binary.Indexed.Homogeneous

    -- Homogeneously-indexed binary relations
    import Relation.Binary.Indexed.Homogeneous.Bundles

    -- Instantiating homogeneously indexed bundles at a particular index
    import Relation.Binary.Indexed.Homogeneous.Construct.At

    -- Homogeneously-indexed binary relations
    import Relation.Binary.Indexed.Homogeneous.Definitions

    -- Homogeneously-indexed binary relations
    import Relation.Binary.Indexed.Homogeneous.Structures

    -- Order-theoretic lattices
    import Relation.Binary.Lattice

    -- Bundles for order-theoretic lattices
    import Relation.Binary.Lattice.Bundles

    -- Definitions for order-theoretic lattices
    import Relation.Binary.Lattice.Definitions

    -- Properties satisfied by bounded join semilattices
    import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice

    -- Properties satisfied by bounded lattice
    import Relation.Binary.Lattice.Properties.BoundedLattice

    -- Properties satisfied by bounded meet semilattices
    import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice

    -- Properties for distributive lattice
    import Relation.Binary.Lattice.Properties.DistributiveLattice

    -- Properties satisfied by Heyting Algebra
    import Relation.Binary.Lattice.Properties.HeytingAlgebra

    -- Properties satisfied by join semilattices
    import Relation.Binary.Lattice.Properties.JoinSemilattice

    -- Properties satisfied by lattices
    import Relation.Binary.Lattice.Properties.Lattice

    -- Properties satisfied by meet semilattices
    import Relation.Binary.Lattice.Properties.MeetSemilattice

    -- Structures for order-theoretic lattices
    import Relation.Binary.Lattice.Structures

    -- Order morphisms
    import Relation.Binary.Morphism

    -- Bundles for morphisms between binary relations
    import Relation.Binary.Morphism.Bundles

    -- The composition of morphisms between binary relations
    import Relation.Binary.Morphism.Construct.Composition

    -- Constant morphisms between binary relations
    import Relation.Binary.Morphism.Construct.Constant

    -- The identity morphism for binary relations
    import Relation.Binary.Morphism.Construct.Identity

    -- The projection morphisms for relational structures arising from the
    -- non-dependent product construction
    import Relation.Binary.Morphism.Construct.Product

    -- Basic definitions for morphisms between algebraic structures
    import Relation.Binary.Morphism.Definitions

    -- Consequences of a monomorphism between orders
    import Relation.Binary.Morphism.OrderMonomorphism

    -- Consequences of a monomorphism between binary relations
    import Relation.Binary.Morphism.RelMonomorphism

    -- Order morphisms
    import Relation.Binary.Morphism.Structures

    -- This module is DEPRECATED. Please use `Relation.Binary.Morphism`
    -- instead.
    import Relation.Binary.OrderMorphism

    -- Apartness properties
    import Relation.Binary.Properties.ApartnessRelation

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.BoundedJoinSemilattice` instead.
    import Relation.Binary.Properties.BoundedJoinSemilattice

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.BoundedLattice` instead.
    import Relation.Binary.Properties.BoundedLattice

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.BoundedMeetSemilattice` instead.
    import Relation.Binary.Properties.BoundedMeetSemilattice

    -- Every decidable setoid induces tight apartness relation.
    import Relation.Binary.Properties.DecSetoid

    -- Properties satisfied by decidable total orders
    import Relation.Binary.Properties.DecTotalOrder

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.DistributiveLattice` instead.
    import Relation.Binary.Properties.DistributiveLattice

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.HeytingAlgebra` instead.
    import Relation.Binary.Properties.HeytingAlgebra

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.JoinSemilattice` instead.
    import Relation.Binary.Properties.JoinSemilattice

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.Lattice` instead.
    import Relation.Binary.Properties.Lattice

    -- This module is DEPRECATED. Please use
    -- `Relation.Binary.Lattice.Properties.MeetSemilattice` instead.
    import Relation.Binary.Properties.MeetSemilattice

    -- Additional properties for setoids
    import Relation.Binary.Properties.PartialSetoid

    -- Properties satisfied by posets
    import Relation.Binary.Properties.Poset

    -- Properties satisfied by preorders
    import Relation.Binary.Properties.Preorder

    -- Additional properties for setoids
    import Relation.Binary.Properties.Setoid

    -- Properties satisfied by strict partial orders
    import Relation.Binary.Properties.StrictPartialOrder

    -- Properties satisfied by strict partial orders
    import Relation.Binary.Properties.StrictTotalOrder

    -- Properties satisfied by total orders
    import Relation.Binary.Properties.TotalOrder

    -- Propositional (intensional) equality
    import Relation.Binary.PropositionalEquality

    -- Propositional (intensional) equality - Algebraic structures
    import Relation.Binary.PropositionalEquality.Algebra

    -- Propositional equality
    import Relation.Binary.PropositionalEquality.Properties

    -- Some code related to propositional equality that relies on the K
    -- rule
    import Relation.Binary.PropositionalEquality.WithK

    -- The basic code for equational reasoning with three relations:
    -- equality and apartness
    import Relation.Binary.Reasoning.Base.Apartness

    -- The basic code for equational reasoning with two relations:
    -- equality and some other ordering.
    import Relation.Binary.Reasoning.Base.Double

    -- The basic code for equational reasoning with a non-reflexive relation
    import Relation.Binary.Reasoning.Base.Partial

    -- The basic code for equational reasoning with a single relation
    import Relation.Binary.Reasoning.Base.Single

    -- The basic code for equational reasoning with three relations:
    -- equality, strict ordering and non-strict ordering.
    import Relation.Binary.Reasoning.Base.Triple

    -- Convenient syntax for "equational reasoning" in multiple Setoids.
    import Relation.Binary.Reasoning.MultiSetoid

    -- Convenient syntax for "equational reasoning" using a partial order
    import Relation.Binary.Reasoning.PartialOrder

    -- Convenient syntax for reasoning with a partial setoid
    import Relation.Binary.Reasoning.PartialSetoid

    -- Convenient syntax for "equational reasoning" using a preorder
    import Relation.Binary.Reasoning.Preorder

    -- Convenient syntax for reasoning with a setoid
    import Relation.Binary.Reasoning.Setoid

    -- Convenient syntax for "equational reasoning" using a strict partial
    -- order.
    import Relation.Binary.Reasoning.StrictPartialOrder

    -- Syntax for the building blocks of equational reasoning modules
    import Relation.Binary.Reasoning.Syntax

    -- Helpers intended to ease the development of "tactics" which use
    -- proof by reflection
    import Relation.Binary.Reflection

    -- Concepts from rewriting theory
    -- Definitions are based on "Term Rewriting Systems" by J.W. Klop
    import Relation.Binary.Rewriting

    -- Structures for homogeneous binary relations
    import Relation.Binary.Structures

    -- Ways to give instances of certain structures where some fields can
    -- be given in terms of others
    import Relation.Binary.Structures.Biased

    -- Typeclasses for use with instance arguments
    import Relation.Binary.TypeClasses

    -- Heterogeneous N-ary Relations
    import Relation.Nary

    -- Operations on nullary relations (like negation and decidability)
    import Relation.Nullary

    -- Notation for freely adding extrema to any set
    import Relation.Nullary.Construct.Add.Extrema

    -- Notation for freely adding an infimum to any set
    import Relation.Nullary.Construct.Add.Infimum

    -- Notation for adding an additional point to any set
    import Relation.Nullary.Construct.Add.Point

    -- Notation for freely adding a supremum to any set
    import Relation.Nullary.Construct.Add.Supremum

    -- Operations on and properties of decidable relations
    import Relation.Nullary.Decidable

    -- This module is DEPRECATED.
    import Relation.Nullary.Implication

    -- Negation indexed by a Level
    import Relation.Nullary.Indexed

    -- Properties of indexed negation
    import Relation.Nullary.Indexed.Negation

    -- A type `A` is irrelevant if all of its elements are equal.
    -- This is also refered to as "A is an h-proposition".
    import Relation.Nullary.Irrelevant

    -- Properties related to negation
    import Relation.Nullary.Negation

    -- This module is DEPRECATED.
    import Relation.Nullary.Product

    -- Recomputable types and their algebra as Harrop formulas
    import Relation.Nullary.Recomputable

    -- Properties of the `Reflects` construct
    import Relation.Nullary.Reflects

    -- This module is DEPRECATED.
    import Relation.Nullary.Sum

    -- A universe of proposition functors, along with some properties
    import Relation.Nullary.Universe

    -- Unary relations
    import Relation.Unary

    -- Algebraic properties of constructions over unary relations
    import Relation.Unary.Algebra

    -- Closures of a unary relation with respect to a binary one.
    import Relation.Unary.Closure.Base

    -- Closure of a unary relation with respect to a preorder
    import Relation.Unary.Closure.Preorder

    -- Closures of a unary relation with respect to a strict partial order
    import Relation.Unary.Closure.StrictPartialOrder

    -- Some properties imply others
    import Relation.Unary.Consequences

    -- Indexed unary relations
    import Relation.Unary.Indexed

    -- Polymorphic versions of standard definitions in Relation.Unary
    import Relation.Unary.Polymorphic

    -- Properties of polymorphic versions of standard definitions in
    -- Relation.Unary
    import Relation.Unary.Polymorphic.Properties

    -- Predicate transformers
    import Relation.Unary.PredicateTransformer

    -- Properties of constructions over unary relations
    import Relation.Unary.Properties

    -- Equality of unary relations
    import Relation.Unary.Relation.Binary.Equality

    -- Order properties of the subset relations _⊆_ and _⊂_
    import Relation.Unary.Relation.Binary.Subset

    -- This module is DEPRECATED, please use `Function.Strict` directly.
    import Strict

    -- ANSI escape codes
    import System.Console.ANSI

    -- A simple tactic for used to automatically compute the function
    -- argument to cong.
    import Tactic.Cong

    -- Reflection-based solver for monoid equalities
    import Tactic.MonoidSolver

    -- A solver that uses reflection to automatically obtain and solve
    -- equations over rings.
    import Tactic.RingSolver

    -- Almost commutative rings
    import Tactic.RingSolver.Core.AlmostCommutativeRing

    -- A type for expressions over a raw ring.
    import Tactic.RingSolver.Core.Expression

    -- Simple implementation of sets of ℕ.
    import Tactic.RingSolver.Core.NatSet

    -- Sparse polynomials in a commutative ring, encoded in Horner normal
    -- form.
    import Tactic.RingSolver.Core.Polynomial.Base

    -- Some specialised instances of the ring solver
    import Tactic.RingSolver.Core.Polynomial.Homomorphism

    -- Homomorphism proofs for addition over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition

    -- Homomorphism proofs for constants over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants

    -- Homomorphism proofs for exponentiation over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation

    -- Lemmas for use in proving the polynomial homomorphism.
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas

    -- Homomorphism proofs for multiplication over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication

    -- Homomorphism proofs for negation over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation

    -- Homomorphism proofs for variables and constants over polynomials
    import Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables

    -- Bundles of parameters for passing to the Ring Solver
    import Tactic.RingSolver.Core.Polynomial.Parameters

    -- Polynomial reasoning
    import Tactic.RingSolver.Core.Polynomial.Reasoning

    -- "Evaluating" a polynomial, using Horner's method.
    import Tactic.RingSolver.Core.Polynomial.Semantics

    -- An implementation of the ring solver that requires you to manually
    -- pass the equation you wish to solve.
    import Tactic.RingSolver.NonReflective

    -- Format strings for Printf and Scanf
    import Text.Format

    -- Format strings for Printf and Scanf
    import Text.Format.Generic

    -- Printf
    import Text.Printf

    -- Generic printf function.
    import Text.Printf.Generic

    -- Regular expressions
    import Text.Regex

    -- Regular expressions: basic types and semantics
    import Text.Regex.Base

    -- Regular expressions: Brzozowski derivative
    import Text.Regex.Derivative.Brzozowski

    -- Properties of regular expressions and their semantics
    import Text.Regex.Properties

    -- Regular expressions: search algorithms
    import Text.Regex.Search

    -- Regular expressions: smart constructors
    -- Computing the Brzozowski derivative of a regular expression may lead
    -- to a blow-up in the size of the expression. To keep it tractable it
    -- is crucial to use smart constructors.
    import Text.Regex.SmartConstructors

    -- Regular expressions acting on strings
    import Text.Regex.String

    -- Fancy display functions for List-based tables
    import Text.Tabular.Base

    -- Fancy display functions for List-based tables
    import Text.Tabular.List

    -- Fancy display functions for Vec-based tables
    import Text.Tabular.Vec