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

-- Note that core modules are not included.


module Everything where

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

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

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

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

-- Relations between properties of functions, such as associativity and
-- commutativity
import Algebra.FunctionProperties.Consequences

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

-- Morphisms between algebraic structures
import Algebra.Morphism

-- Some defined operations (multiplication by natural number and
-- exponentiation)
import Algebra.Operations.CommutativeMonoid

-- Some defined operations (multiplication by natural number and
-- exponentiation)
import Algebra.Operations.Semiring

-- Some derivable properties
import Algebra.Properties.AbelianGroup

-- Some derivable properties
import Algebra.Properties.BooleanAlgebra

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

-- Some derivable properties
import Algebra.Properties.CommutativeMonoid

-- Some derivable properties
import Algebra.Properties.DistributiveLattice

-- Some derivable properties
import Algebra.Properties.Group

-- Some derivable properties
import Algebra.Properties.Lattice

-- Some derivable properties
import Algebra.Properties.Ring

-- Some derivable properties
import Algebra.Properties.Semilattice

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

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

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

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

-- Solver for monoid equalities
import Algebra.Solver.Monoid

-- 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

-- 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

-- Applicative functors
import Category.Applicative

-- Indexed applicative functors
import Category.Applicative.Indexed

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

-- Comonads
import Category.Comonad

-- Functors
import Category.Functor

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

-- Monads
import Category.Monad

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

-- Indexed monads
import Category.Monad.Indexed

-- The partiality monad
import Category.Monad.Partiality

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

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

-- The state monad
import Category.Monad.State

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

-- Conat Literals
import Codata.Cofin.Literals

-- The Colist type and some operations
import Codata.Colist

-- Bisimilarity for Colists
import Codata.Colist.Bisimilarity

-- A categorical view of Colist
import Codata.Colist.Categorical

-- Properties of operations on the Colist type
import Codata.Colist.Properties

-- The Conat type and some operations
import Codata.Conat

-- Bisimilarity for Conats
import Codata.Conat.Bisimilarity

-- Conat Literals
import Codata.Conat.Literals

-- Properties for Conats
import Codata.Conat.Properties

-- The Covec type and some operations
import Codata.Covec

-- Bisimilarity for Covecs
import Codata.Covec.Bisimilarity

-- A categorical view of Covec
import Codata.Covec.Categorical

-- Properties of operations on the Covec type
import Codata.Covec.Properties

-- The Cowriter type and some operations
import Codata.Cowriter

-- The Delay type and some operations
import Codata.Delay

-- Bisimilarity for the Delay type
import Codata.Delay.Bisimilarity

-- A categorical view of Delay
import Codata.Delay.Categorical

-- Properties of operations on the Delay type
import Codata.Delay.Properties

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

-- Bisimilarity for M-types
import Codata.M.Bisimilarity

-- Properties of operations on M-types
import Codata.M.Properties

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

-- Coinductive lists
import Codata.Musical.Colist

-- Infinite merge operation for coinductive lists
import Codata.Musical.Colist.Infinite-merge

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

-- Costrings
import Codata.Musical.Costring

-- Coinductive vectors
import Codata.Musical.Covec

-- 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

-- Streams
import Codata.Musical.Stream

-- The Stream type and some operations
import Codata.Stream

-- Bisimilarity for Streams
import Codata.Stream.Bisimilarity

-- A categorical view of Stream
import Codata.Stream.Categorical

-- Properties of operations on the Stream type
import Codata.Stream.Properties

-- The Thunk wrappers for sized codata, copredicates and corelations
import Codata.Thunk

-- AVL trees
import Data.AVL

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

-- Indexed AVL trees
import Data.AVL.Indexed

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

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

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

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

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

-- A binary representation of natural numbers
import Data.Bin

-- Properties of the binary representation of natural numbers
import Data.Bin.Properties

-- Booleans
import Data.Bool

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

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

-- Showing booleans
import Data.Bool.Show

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

-- Bounded vectors
import Data.BoundedVec

-- Bounded vectors (inefficient, concrete implementation)
import Data.BoundedVec.Inefficient

-- Characters
import Data.Char

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

-- 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

-- 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

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

-- 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

-- 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

-- Empty type
import Data.Empty

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

-- Finite sets
import Data.Fin

-- Finite sets
import Data.Fin.Base

-- Decision procedures for finite sets and subsets of finite sets
import Data.Fin.Dec

-- Fin Literals
import Data.Fin.Literals

-- 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

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

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

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

-- Substitutions
import Data.Fin.Substitution

-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas
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

-- Floats
import Data.Float

-- Unsafe Float operations
import Data.Float.Unsafe

-- 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

-- Integer Literals
import Data.Integer.Literals

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

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

-- Lists
import Data.List

-- This module is DEPRECATED. Please use Data.List.Relation.Unary.All
-- directly.
import Data.List.All

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Unary.Any.Properties directly.
import Data.List.All.Properties

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

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

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

-- A categorical view of List
import Data.List.Categorical

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

-- 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

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

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

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

-- A categorical view of List⁺
import Data.List.NonEmpty.Categorical

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

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

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Unary.Any.Properties directly.
import Data.List.Relation.BagAndSetEquality

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

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

-- Decidable equality over lists parameterised by some setoid
import Data.List.Relation.Binary.Equality.DecSetoid

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

-- Equality over lists parameterised by some setoid
import Data.List.Relation.Binary.Equality.Setoid

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

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

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

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

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

-- 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

-- 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

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

-- 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

-- 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

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.DecPropositional directly.
import Data.List.Relation.Equality.DecPropositional

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.DecSetoid directly.
import Data.List.Relation.Equality.DecSetoid

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.Propositional directly.
import Data.List.Relation.Equality.Propositional

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.Setoid directly.
import Data.List.Relation.Equality.Setoid

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Lex.NonStrict directly.
import Data.List.Relation.Lex.NonStrict

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Lex.Strict directly.
import Data.List.Relation.Lex.Strict

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Inductive directly.
import Data.List.Relation.Permutation.Inductive

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Inductive.Properties directly.
import Data.List.Relation.Permutation.Inductive.Properties

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Pointwise directly.
import Data.List.Relation.Pointwise

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Sublist.Propositional directly.
import Data.List.Relation.Sublist.Propositional

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Sublist.Propositional.Properties directly.
import Data.List.Relation.Sublist.Propositional.Properties

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Propositional directly.
import Data.List.Relation.Subset.Propositional

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Propositional.Properties directly.
import Data.List.Relation.Subset.Propositional.Properties

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Setoid directly.
import Data.List.Relation.Subset.Setoid

-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Setoid.Properties directly.
import Data.List.Relation.Subset.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 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

-- 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

-- Reverse view
import Data.List.Reverse

-- Automatic solvers for equations over lists
import Data.List.Solver

-- 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

-- A categorical view of Maybe
import Data.Maybe.Categorical

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

-- 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

-- 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

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

-- Least common multiple
import Data.Nat.LCM

-- Natural Literals
import Data.Nat.Literals

-- Primality
import Data.Nat.Primality

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

-- Showing natural numbers
import Data.Nat.Show

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

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

-- Transitive closures
import Data.Plus

-- Products
import Data.Product

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

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

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

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

-- Base definitions for the right-biased universe-sensitive functor
-- and monad instances for the Product type.
import Data.Product.Categorical.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

-- Dependent product combinators for setoid equality preserving
-- functions
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

-- N-ary products
import Data.Product.N-ary

-- A categorical view of N-ary products
import Data.Product.N-ary.Categorical

-- Properties of n-ary products
import Data.Product.N-ary.Properties

-- Properties of products
import Data.Product.Properties

-- 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

-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Lex.NonStrict directly.
import Data.Product.Relation.Lex.NonStrict

-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Lex.Strict directly.
import Data.Product.Relation.Lex.Strict

-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Pointwise.Dependent directly.
import Data.Product.Relation.Pointwise.Dependent

-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Pointwise.NonDependent directly.
import Data.Product.Relation.Pointwise.NonDependent

-- Rational numbers
import Data.Rational

-- Rational numbers
import Data.Rational.Base

-- Rational Literals
import Data.Rational.Literals

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

-- Reflexive closures
import Data.ReflexiveClosure

-- Signs
import Data.Sign

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

-- The reflexive transitive closures of McBride, Norell and Jansson
import Data.Star

-- 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

-- Some properties related to Data.Star
import Data.Star.Properties

-- 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

-- String Literals
import Data.String.Literals

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

-- Unsafe String operations and proofs
import Data.String.Unsafe

-- Sums (disjoint unions)
import Data.Sum

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

-- Usage examples of the categorical view of the Sum type
import Data.Sum.Categorical.Examples

-- A Categorical view of the Sum type (Left-biased)
import Data.Sum.Categorical.Left

-- A Categorical view of the Sum type (Right-biased)
import Data.Sum.Categorical.Right

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

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

-- 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

-- This module is DEPRECATED. Please use
-- Data.Sum.Relation.Binary.LeftOrder directly.
import Data.Sum.Relation.LeftOrder

-- This module is DEPRECATED. Please use
-- Data.Sum.Relation.Binary.Pointwise directly.
import Data.Sum.Relation.Pointwise

-- Fixed-size tables of values, implemented as functions from 'Fin n'.
-- Similar to 'Data.Vec', but focusing on ease of retrieval instead of
-- ease of adding and removing elements.
import Data.Table

-- Tables, basic types and operations
import Data.Table.Base

-- Table-related properties
import Data.Table.Properties

-- Pointwise table equality
import Data.Table.Relation.Binary.Equality

-- This module is DEPRECATED. Please use
-- Data.Table.Relation.Binary.Equality directly.
import Data.Table.Relation.Equality

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

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

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

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

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

-- Properties of These
import Data.These.Properties

-- Some unit types
import Data.Unit

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

-- Some unit types
import Data.Unit.NonEta

-- Vectors
import Data.Vec

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.All directly.
import Data.Vec.All

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.All.Properties directly.
import Data.Vec.All.Properties

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

-- A categorical view of Vec
import Data.Vec.Categorical

-- 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

-- 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

-- 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

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.DecPropositional directly.
import Data.Vec.Relation.Equality.DecPropositional

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.DecSetoid directly.
import Data.Vec.Relation.Equality.DecSetoid

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Propositional directly.
import Data.Vec.Relation.Equality.Propositional

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Setoid directly.
import Data.Vec.Relation.Equality.Setoid

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Pointwise.Extensional directly.
import Data.Vec.Relation.Pointwise.Extensional

-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Pointwise.Extensional directly.
import Data.Vec.Relation.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 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

-- 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

-- Machine words
import Data.Word

-- Unsafe machine word operations
import Data.Word.Unsafe

-- Printing Strings During Evaluation
import Debug.Trace

-- Type(s) used (only) when calling out to Haskell via the FFI
import Foreign.Haskell

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

-- Bijections
import Function.Bijection

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

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

-- Function setoids and related constructions
import Function.Equality

-- Equivalence (coinhabitance)
import Function.Equivalence

-- Half adjoint equivalences
import Function.HalfAdjointEquivalence

-- A categorical view of the identity function
import Function.Identity.Categorical

-- Injections
import Function.Injection

-- Inverses
import Function.Inverse

-- Left inverses
import Function.LeftInverse

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

-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
import Function.Related

-- 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

-- Surjections
import Function.Surjection

-- IO
import IO

-- Primitive IO: simple bindings to Haskell types and functions
import IO.Primitive

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

-- Lexicographic induction
import Induction.Lexicographic

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

-- Well-founded induction
import Induction.WellFounded

-- Universe levels
import Level

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

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

-- Support for reflection
import Reflection

-- Properties of homogeneous binary relations
import Relation.Binary

-- 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 non-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

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

-- 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

-- 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

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

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

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

-- 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

-- 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

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

-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.Setoid module directly.
import Relation.Binary.EqReasoning

-- Equivalence closures of binary relations
import Relation.Binary.EquivalenceClosure

-- 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

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

-- 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

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

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

-- Order morphisms
import Relation.Binary.OrderMorphism

-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.PartialOrder module directly.
import Relation.Binary.PartialOrderReasoning

-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.Preorder module directly.
import Relation.Binary.PreorderReasoning

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

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

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

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

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

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

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

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

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

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

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

-- 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

-- An equality postulate which evaluates
import Relation.Binary.PropositionalEquality.TrustMe

-- Some code related to propositional equality that relies on the K
-- rule
import Relation.Binary.PropositionalEquality.WithK

-- 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 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 "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

-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
import Relation.Binary.Reflection

-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.MultiSetoid module directly.
import Relation.Binary.SetoidReasoning

-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.StrictPartialOrder module directly.
import Relation.Binary.StrictPartialOrderReasoning

-- Symmetric closures of binary relations
import Relation.Binary.SymmetricClosure

-- 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

-- Implications of nullary relations
import Relation.Nullary.Implication

-- Properties related to negation
import Relation.Nullary.Negation

-- Products of nullary relations
import Relation.Nullary.Product

-- Sums of nullary relations
import Relation.Nullary.Sum

-- A universe of proposition functors, along with some properties
import Relation.Nullary.Universe

-- Unary relations
import Relation.Unary

-- 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

-- Indexed unary relations
import Relation.Unary.Indexed

-- Predicate transformers
import Relation.Unary.PredicateTransformer

-- Properties of constructions over unary relations
import Relation.Unary.Properties

-- Sizes for Agda's sized types
import Size

-- Strictness combinators
import Strict

-- Universes
import Universe