All.agda

{-# OPTIONS --sized-types --guardedness --cubical #-}

-- Note: This module is not meant to be imported.
module All where

-- import All
-- import Automaton.Deterministic.Accessible
-- import Automaton.Deterministic.FormalLanguage
-- import Automaton.Deterministic.Oper
import Automaton.Deterministic.Proofs.Automaton
-- import Automaton.Deterministic.Proofs
-- import Automaton.Deterministic.Relations
import Automaton.Deterministic
import Automaton.FormalLanguage
-- import Automaton.NonDeterministic
-- import Automaton.Pushdown
-- import Automaton.TuringMachine
import Automaton
import BidirectionalFunction.Equiv
import BidirectionalFunction
import Char.Decidable
import Char.Functions
import Char.Proofs
import Char
import Data.Any
import Data.BinaryTree.Functions.Proofs
import Data.BinaryTree.Functions
import Data.BinaryTree.Heap
import Data.BinaryTree.Properties
import Data.BinaryTree
import Data.Boolean.Decidable
import Data.Boolean.Equiv.Path
import Data.Boolean.Functions
import Data.Boolean.NaryOperators
import Data.Boolean.Numeral
import Data.Boolean.Operators
import Data.Boolean.Proofs
import Data.Boolean.Stmt.Logic
import Data.Boolean.Stmt.Proofs
import Data.Boolean.Stmt
import Data.Boolean
import Data.DependentWidthTree
import Data.DifferenceList
import Data.DynamicTree
import Data.Either.Equiv.Id
import Data.Either.Equiv
import Data.Either.Multi
import Data.Either.Proofs.Map
import Data.Either.Proofs
import Data.Either.Setoid
import Data.Either
import Data.FixedTree.Properties
import Data.FixedTree
import Data.IndexedList
import Data.Iterator
import Data.List.Categorical
import Data.List.Combinatorics.Proofs
import Data.List.Combinatorics
import Data.List.Decidable
import Data.List.Equiv.Id
import Data.List.Equiv
import Data.List.Functions.Multi
import Data.List.Functions.Positional
import Data.List.Functions.Proofs.Positional
import Data.List.Functions.Tuple
import Data.List.Functions
import Data.List.FunctionsProven.Proofs
import Data.List.FunctionsProven
import Data.List.Iterable
import Data.List.Proofs.Index
import Data.List.Proofs.Length
import Data.List.Proofs.Reverse
import Data.List.Proofs.Simple
import Data.List.Proofs
import Data.List.Relation.Enum.Proofs
import Data.List.Relation.Enum
import Data.List.Relation.Fixes
import Data.List.Relation.Membership.Functions
import Data.List.Relation.Membership.Proofs
import Data.List.Relation.Membership
import Data.List.Relation.Pairwise.Proofs
import Data.List.Relation.Pairwise
import Data.List.Relation.Permutation.ByInsertion.Height
import Data.List.Relation.Permutation.ByInsertion.Mapping
import Data.List.Relation.Permutation.ByInsertion.Oper.Proofs
import Data.List.Relation.Permutation.ByInsertion.Oper
import Data.List.Relation.Permutation.ByInsertion.Proofs
import Data.List.Relation.Permutation.ByInsertion
import Data.List.Relation.Permutation.Proofs
import Data.List.Relation.Permutation
import Data.List.Relation.Quantification.Existential.Functions
import Data.List.Relation.Quantification.Existential.Proofs
import Data.List.Relation.Quantification.Proofs
import Data.List.Relation.Quantification.Uniqueness
import Data.List.Relation.Quantification.Universal.Functions
import Data.List.Relation.Quantification.Universal.Proofs
import Data.List.Relation.Quantification
import Data.List.Relation.Sublist.Proofs
import Data.List.Relation.Sublist
import Data.List.Relation
import Data.List.Setoid
import Data.List.Size
import Data.List.SizeOrdering
import Data.List.Sorting.Functions
import Data.List.Sorting.HeapSort
import Data.List.Sorting.InsertionSort
import Data.List.Sorting.MergeSort
import Data.List.Sorting.Proofs
import Data.List.Sorting.QuickSort
import Data.List.Sorting.SelectionSort
import Data.List.Sorting
import Data.List.Structure.Monoid
import Data.List
import Data.ListNonEmpty
import Data.ListSized.Functions
import Data.ListSized.Proofs
import Data.ListSized
import Data.Option.Categorical
import Data.Option.Equiv.Id
import Data.Option.Equiv.Path
import Data.Option.Equiv
import Data.Option.Functions.Unmap.Proofs
import Data.Option.Functions.Unmap
import Data.Option.Functions
import Data.Option.Iterable
import Data.Option.Proofs
import Data.Option.Quantifiers.Proofs
import Data.Option.Quantifiers
import Data.Option.Relation
import Data.Option.Setoid
import Data.Option
import Data.Proofs
import Data.Tuple.Category
import Data.Tuple.Equiv.Id
import Data.Tuple.Equiv
import Data.Tuple.Equivalence
import Data.Tuple.Function
import Data.Tuple.List
import Data.Tuple.Proofs
import Data.Tuple.Raise
import Data.Tuple.RaiseTypeᵣ.Functions
import Data.Tuple.RaiseTypeᵣ
import Data.Tuple.Raiseᵣ.Functions
import Data.Tuple.Raiseᵣ.Iterable
import Data.Tuple.Raiseᵣ.Proofs
import Data.Tuple.Raiseᵣ
import Data.Tuple.Raiseₗ
import Data.Tuple
import Data.UniqueList
import Data.Wrap
import Data
import Dataω.Tuple
import DependentFunction.Equiv
import DependentFunction
import DependentFunctional
import FFI.IO
import FFI.MachineWord
import Float
-- import FormalLanguage.ContextFreeGrammar
-- import FormalLanguage.Equals
import FormalLanguage.Oper
-- import FormalLanguage.Proofs
-- import FormalLanguage
import FormalLanguage2.Equals
import FormalLanguage2.Oper
import FormalLanguage2.Proofs
import FormalLanguage2
import Formalization.ClassicalPredicateLogic.Semantics
import Formalization.ClassicalPredicateLogic.Syntax.Substitution
import Formalization.ClassicalPredicateLogic.Syntax
import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Consistency
import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Proofs
-- import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Tree
import Formalization.ClassicalPropositionalLogic.NaturalDeduction
import Formalization.ClassicalPropositionalLogic.Place
import Formalization.ClassicalPropositionalLogic.Semantics.Proofs
import Formalization.ClassicalPropositionalLogic.Semantics
-- import Formalization.ClassicalPropositionalLogic.SequentCalculus
import Formalization.ClassicalPropositionalLogic.Syntax.Proofs
import Formalization.ClassicalPropositionalLogic.Syntax
import Formalization.ClassicalPropositionalLogic.TruthTable
-- import Formalization.ClassicalPropositionalLogic
-- import Formalization.FunctionalML
-- import Formalization.ImperativePL
import Formalization.LambdaCalculus.ByVarCount.ByIndices.Semantics.CallByName
import Formalization.LambdaCalculus.ByVarCount.ByIndices.Semantics.CallByValue
import Formalization.LambdaCalculus.ByVarCount.ByIndices.Semantics.Reduction.Proofs
import Formalization.LambdaCalculus.ByVarCount.ByIndices.Semantics.Reduction
import Formalization.LambdaCalculus.ByVarCount.ByIndices.Terms.Combinators
import Formalization.LambdaCalculus.ByVarCount.ByIndices
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Equals
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Evaluator
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Operational
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Operators.Normal
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Operators
-- import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Reduction.Proofs.Properties
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Reduction.Proofs
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Semantics.Reduction
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Terms.ApplyIterated
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Terms.Boolean
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Terms.ChurchNumeral
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Terms.Combinators
import Formalization.LambdaCalculus.ByVarCount.ByLevels.Terms.Tuple
import Formalization.LambdaCalculus.ByVarCount.ByLevels
import Formalization.LambdaCalculus.ByVarCount.Functions.Proofs
import Formalization.LambdaCalculus.ByVarCount.Functions
import Formalization.LambdaCalculus.ByVarCount.Semantics
import Formalization.LambdaCalculus.ByVarCount.Syntax.ExplicitLambda
import Formalization.LambdaCalculus.ByVarCount.Syntax.ImplicitLambda
import Formalization.LambdaCalculus.ByVarCount.Syntax.VarNumeral
import Formalization.LambdaCalculus.ByVarCount
-- import Formalization.LambdaCalculus.ByVarIndex
import Formalization.Monoid
import Formalization.Polynomial
import Formalization.PredicateLogic.Classical.NaturalDeduction
-- import Formalization.PredicateLogic.Classical.Semantics.Homomorphism
import Formalization.PredicateLogic.Classical.Semantics.Satisfaction
import Formalization.PredicateLogic.Classical.Semantics
import Formalization.PredicateLogic.Classical.SequentCalculus
import Formalization.PredicateLogic.Constructive.NaturalDeduction
-- import Formalization.PredicateLogic.Constructive.SequentCalculus
-- import Formalization.PredicateLogic.Minimal.NaturalDeduction.NegativeTranslations
import Formalization.PredicateLogic.Minimal.NaturalDeduction.Tree
import Formalization.PredicateLogic.Minimal.NaturalDeduction
-- import Formalization.PredicateLogic.Minimal.SequentCalculus
import Formalization.PredicateLogic.Signature
import Formalization.PredicateLogic.Syntax.NegativeTranslations
import Formalization.PredicateLogic.Syntax.Substitution
import Formalization.PredicateLogic.Syntax.Tree
import Formalization.PredicateLogic.Syntax
import Formalization.PrimitiveRecursion
-- import Formalization.PureTypeSystem
import Formalization.RecursiveFunction
import Formalization.RegularExpression.Language
import Formalization.RegularExpression.Relations
import Formalization.RegularExpression
import Formalization.SKICombinatorCalculus
import Formalization.Semigroup
import Formalization.SimplyTypedLambdaCalculus
import Function.Category.Functors.Hom
import Function.Category.Functors.LvlUp
import Function.Category.Monoidal
import Function.Category.Proofs
import Function.Category
import Function.DomainRaise
import Function.Domains.Proofs
import Function.Domains
import Function.Equals.Multi
import Function.Equals.Proofs
import Function.Equals
import Function.EqualsRaw
import Function.Equiv.Proofs
import Function.Equiv
import Function.Inverse
import Function.Inverseᵣ
import Function.Inverseₗ
import Function.Iteration.Order
import Function.Iteration.Proofs
import Function.Iteration
import Function.Multi.Functions
import Function.Multi
import Function.Multi₌.Functions
import Function.Multi₌
import Function.Names
import Function.PointwiseStructure
import Function.Proofs.Classical
import Function.Proofs
import Function.Signature.IndexedCategory
import Function.Structure
import Function
import Functional.Categorical
import Functional.Combinations
import Functional.Implicit
import Functional.Instance
import Functional.Irrelevant
import Functional.NonNormalizing
import Functional.Setoid
import Functional
-- import Geometry.Axioms
-- import Geometry.HilbertAxioms
import Graph.Oper
import Graph.Properties.Proofs
import Graph.Properties
import Graph.Walk.Category
import Graph.Walk.Functions.Proofs
import Graph.Walk.Functions
import Graph.Walk.Proofs
import Graph.Walk.Properties
import Graph.Walk
import Graph
import ImplicitFunction.Category
import Iterator
import Js
import Lang.Function
import Lang.Inspect
import Lang.Irrelevance.Convertable
import Lang.Irrelevance.Squash
import Lang.Irrelevance
import Lang.Reflection.DoNotation
import Lang.Reflection
import Lang.Size
import Lang.Templates.Fractions
import Lang.Templates.Order
import Lang.Vars.Structure.Operator
import Logic.Choice.Proofs
import Logic.Choice
import Logic.Classical.DoubleNegated
import Logic.Classical
import Logic.DiagonalMethod
import Logic.IntroInstances
import Logic.Names
import Logic.Predicate.Equiv
import Logic.Predicate.Multi
import Logic.Predicate.Proofs
import Logic.Predicate.Theorems
import Logic.Predicate
import Logic.Propositional.Equiv
import Logic.Propositional.Proofs.Structures
import Logic.Propositional.Theorems
import Logic.Propositional.Xor.Functions
import Logic.Propositional.Xor.Proofs
import Logic.Propositional.Xor
import Logic.Propositional
import Logic.WeaklyClassical
import Logic
import Lvl.Decidable
import Lvl.Functions
import Lvl.MultiFunctions.Proofs
import Lvl.MultiFunctions
import Lvl.Order
import Lvl.Proofs
import Lvl.Up.Equiv
import Lvl.Up.Equivalence
import Lvl.Up.Proofs
import Lvl
import Main
import Numeral.Bits
import Numeral.Charge.Oper
import Numeral.Charge.Proofs.Bool
import Numeral.Charge.Proofs
import Numeral.Charge
import Numeral.CoordinateVector.List
import Numeral.CoordinateVector.Proofs
import Numeral.CoordinateVector.Relations
import Numeral.CoordinateVector
import Numeral.Finite.Bound.Proofs
import Numeral.Finite.Bound.Substitution
import Numeral.Finite.Bound
import Numeral.Finite.Category.Simplex
import Numeral.Finite.Category
import Numeral.Finite.Conversions
import Numeral.Finite.Decidable.Quantifiers
import Numeral.Finite.Decidable
import Numeral.Finite.Equiv
import Numeral.Finite.Equiv2
import Numeral.Finite.Functions.Proofs
import Numeral.Finite.Functions
import Numeral.Finite.LinearSearch.Proofs.FindAll
import Numeral.Finite.LinearSearch.Proofs.FindMax
import Numeral.Finite.LinearSearch.Proofs.FindMin
import Numeral.Finite.LinearSearch
-- import Numeral.Finite.Oper.Bounded.Proofs.fromℕ
import Numeral.Finite.Oper.Bounded.Proofs.𝐏
import Numeral.Finite.Oper.Bounded.Proofs.𝐒
import Numeral.Finite.Oper.Bounded
import Numeral.Finite.Oper.Comparisons.Proofs
import Numeral.Finite.Oper.Comparisons
import Numeral.Finite.Oper.Exact.Proofs
import Numeral.Finite.Oper.Proofs
import Numeral.Finite.Oper.Wrapping.Proofs
import Numeral.Finite.Oper.Wrapping
import Numeral.Finite.Oper
import Numeral.Finite.Proofs
import Numeral.Finite.Recursion
import Numeral.Finite.Relation.Order.Proofs
import Numeral.Finite.Relation.Order
import Numeral.Finite.Relation.Order2
import Numeral.Finite.Relation
import Numeral.Finite.Sequence
import Numeral.Finite.SequenceTransform.Proofs
import Numeral.Finite.SequenceTransform
import Numeral.Finite.Type
import Numeral.Finite
import Numeral.FixedPositional
import Numeral.Integer.Construction.Proofs
import Numeral.Integer.Construction
import Numeral.Integer.Function.Proofs.Simple
import Numeral.Integer.Function.Proofs
import Numeral.Integer.Function
import Numeral.Integer.Induction
import Numeral.Integer.Oper.Comparisons
import Numeral.Integer.Oper.Proofs
import Numeral.Integer.Oper
import Numeral.Integer.Proofs
import Numeral.Integer.Relation.Divisibility.Proofs
import Numeral.Integer.Relation.Divisibility
import Numeral.Integer.Relation.Order
import Numeral.Integer.Relation
import Numeral.Integer.Sign
import Numeral.Integer
-- import Numeral.Matrix.OverField
import Numeral.Matrix.Proofs
-- import Numeral.Matrix.Relations
import Numeral.Matrix
import Numeral.Natural.Combinatorics.Multi
import Numeral.Natural.Combinatorics.Proofs
import Numeral.Natural.Combinatorics
import Numeral.Natural.Coprime.Decidable
import Numeral.Natural.Coprime.Proofs
import Numeral.Natural.Coprime.Tree
import Numeral.Natural.Coprime
import Numeral.Natural.Decidable
import Numeral.Natural.Equiv.Id
import Numeral.Natural.Equiv.Path
import Numeral.Natural.Function.Coprimalize.Proofs
import Numeral.Natural.Function.Coprimalize
import Numeral.Natural.Function.Divisor.Proofs
import Numeral.Natural.Function.Divisor
import Numeral.Natural.Function.FlooredLogarithm
import Numeral.Natural.Function.GcdLcm.Proofs
import Numeral.Natural.Function.GreatestCommonDivisor.Algorithm
import Numeral.Natural.Function.GreatestCommonDivisor.Extended.Proofs
import Numeral.Natural.Function.GreatestCommonDivisor.Extended
import Numeral.Natural.Function.GreatestCommonDivisor.Proofs.Distributivity
import Numeral.Natural.Function.GreatestCommonDivisor.Proofs
import Numeral.Natural.Function.GreatestCommonDivisor.Relation.Existence
import Numeral.Natural.Function.GreatestCommonDivisor.Relation.Proofs
import Numeral.Natural.Function.GreatestCommonDivisor
import Numeral.Natural.Function.LeastCommonMultiple.Proofs
import Numeral.Natural.Function.LeastCommonMultiple.Relation.Proofs
import Numeral.Natural.Function.LeastCommonMultiple
import Numeral.Natural.Function.PrimeDivisor.Proofs
import Numeral.Natural.Function.PrimeDivisor
import Numeral.Natural.Function.Proofs
import Numeral.Natural.Function
import Numeral.Natural.Induction.Proofs
import Numeral.Natural.Induction
import Numeral.Natural.Inductions.Proofs
import Numeral.Natural.Inductions
import Numeral.Natural.LinearSearch.Proofs
import Numeral.Natural.LinearSearch
import Numeral.Natural.Oper.CeiledDivision.Proofs
import Numeral.Natural.Oper.CeiledDivision
import Numeral.Natural.Oper.Comparisons.Proofs
import Numeral.Natural.Oper.Comparisons
import Numeral.Natural.Oper.DivMod.Proofs
import Numeral.Natural.Oper.Divisibility
import Numeral.Natural.Oper.FlooredDivision.Proofs.Algorithm
import Numeral.Natural.Oper.FlooredDivision.Proofs.Compatibility
import Numeral.Natural.Oper.FlooredDivision.Proofs.Decidable
import Numeral.Natural.Oper.FlooredDivision.Proofs.DivisibilityWithRemainder
import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
import Numeral.Natural.Oper.FlooredDivision.Proofs
import Numeral.Natural.Oper.FlooredDivision
import Numeral.Natural.Oper.Modulo.Proofs.Algorithm
import Numeral.Natural.Oper.Modulo.Proofs.DivisibilityWithRemainder
import Numeral.Natural.Oper.Modulo.Proofs.Elim
import Numeral.Natural.Oper.Modulo.Proofs
import Numeral.Natural.Oper.Modulo.Unclosed
import Numeral.Natural.Oper.Modulo
-- import Numeral.Natural.Oper.Proofs.Elemantary
-- import Numeral.Natural.Oper.Proofs.Iteration
import Numeral.Natural.Oper.Proofs.Multiplication
import Numeral.Natural.Oper.Proofs.Order
import Numeral.Natural.Oper.Proofs.Rewrite
-- import Numeral.Natural.Oper.Proofs.Structure
import Numeral.Natural.Oper.Proofs
import Numeral.Natural.Oper
import Numeral.Natural.Prime.Decidable
import Numeral.Natural.Prime.Proofs.FromDividesProduct
import Numeral.Natural.Prime.Proofs.Product
import Numeral.Natural.Prime.Proofs.Representation
import Numeral.Natural.Prime.Proofs.Size
import Numeral.Natural.Prime.Proofs
import Numeral.Natural.Prime
import Numeral.Natural.Proofs.HLevel
import Numeral.Natural.Proofs
import Numeral.Natural.Relation.Divisibility.Decidable
import Numeral.Natural.Relation.Divisibility.Proofs.FlooredDivision
import Numeral.Natural.Relation.Divisibility.Proofs.List
import Numeral.Natural.Relation.Divisibility.Proofs.Modulo
import Numeral.Natural.Relation.Divisibility.Proofs.Productᵣ
import Numeral.Natural.Relation.Divisibility.Proofs.Productₗ
import Numeral.Natural.Relation.Divisibility.Proofs
import Numeral.Natural.Relation.Divisibility.Strict
import Numeral.Natural.Relation.Divisibility.Two
import Numeral.Natural.Relation.Divisibility
import Numeral.Natural.Relation.DivisibilityWithRemainder.Proofs
import Numeral.Natural.Relation.DivisibilityWithRemainder
import Numeral.Natural.Relation.ModuloCongruence.Equiv
import Numeral.Natural.Relation.ModuloCongruence.Proofs
import Numeral.Natural.Relation.ModuloCongruence
import Numeral.Natural.Relation.Order.Category
import Numeral.Natural.Relation.Order.Classical
import Numeral.Natural.Relation.Order.Decidable
import Numeral.Natural.Relation.Order.Existence.Proofs
import Numeral.Natural.Relation.Order.Existence
import Numeral.Natural.Relation.Order.Proofs
import Numeral.Natural.Relation.Order
import Numeral.Natural.Relation.Proofs
import Numeral.Natural.Relation.Properties
import Numeral.Natural.Relation
import Numeral.Natural.Sequence.Proofs
import Numeral.Natural.Sequence
import Numeral.Natural.String
import Numeral.Natural.TotalOper
import Numeral.Natural.UnclosedOper
import Numeral.Natural
import Numeral.NonNegativeRational
import Numeral.Ordinal
import Numeral.PositiveInteger.Oper.Proofs
import Numeral.PositiveInteger.Oper
import Numeral.PositiveInteger
-- import Numeral.Rational.AlterAdd
import Numeral.Rational.Proofs
-- import Numeral.Rational.SternBrocot
import Numeral.Rational
import Numeral.Sign.Oper
import Numeral.Sign.Proofs
import Numeral.Sign
import Operator.Equals
import Operator.Summation.Proofs
import Operator.Summation.Range.Proofs
import Operator.Summation.Range
import Operator.Summation
import Operator.Summation2
import Operator.Summation3
-- import Operator.Summation4
import Operator.Summation5
-- import Operator.Summation6
-- import Prop.Squash
-- import Prop
import ReductionSystem
import Relator.Category
import Relator.Congruence.Proofs
import Relator.Congruence
import Relator.Converse
import Relator.Equals.Category
import Relator.Equals.Proofs.Equiv
import Relator.Equals.Proofs.Equivalence
import Relator.Equals.Proofs
import Relator.Equals
import Relator.Ordering.Proofs
import Relator.Ordering
import Relator.ReflexiveTransitiveClosure.Proofs
import Relator.ReflexiveTransitiveClosure
import Relator.Sets
import Sets.BoolSet
import Sets.ExtensionalBoolSet
-- import Sets.ExtensionalPredicateSet.SetLike
import Sets.ExtensionalPredicateSet
import Sets.ImageSet.Oper
-- import Sets.ImageSet.SetLike
import Sets.ImageSet
import Sets.IterativeSet.Oper.Proofs
import Sets.IterativeSet.Oper
import Sets.IterativeSet.Relator.Proofs
import Sets.IterativeSet.Relator
import Sets.IterativeSet
import Sets.IterativeUSet
import Sets.PredicateSet.Listable
import Sets.PredicateSet
import Signature.Algebraic
import Signature.IndexedCategory.Functor
import Signature.IndexedCategory
import Sized.Data.List
import Stream.Iterable
import Stream
import String.Decidable
import String.Functions
import String.Proofs
import String
import Structure.Categorical.Functor.Properties
import Structure.Categorical.Functor
import Structure.Categorical.Names
import Structure.Categorical.Proofs
import Structure.Categorical.Properties
import Structure.Category.Action
import Structure.Category.Adjunction
import Structure.Category.Bifunctor
import Structure.Category.Categories
import Structure.Category.Category
import Structure.Category.CoMonad
import Structure.Category.Comma
import Structure.Category.Dual
import Structure.Category.Enriched.Category
import Structure.Category.Enriched.Group
import Structure.Category.Enriched.Monoid
-- import Structure.Category.Equiv
-- import Structure.Category.Foldable
import Structure.Category.Functor.Category
import Structure.Category.Functor.Contravariant
import Structure.Category.Functor.Equiv
import Structure.Category.Functor.Functors.Proofs
import Structure.Category.Functor.Functors
import Structure.Category.Functor.Proofs
import Structure.Category.Functor
import Structure.Category.Monad.Category
import Structure.Category.Monad.ExtensionSystem.Proofs
import Structure.Category.Monad.ExtensionSystem
import Structure.Category.Monad
import Structure.Category.Monoidal.Diagonal
import Structure.Category.Monoidal.Functor
-- import Structure.Category.Monoidal
import Structure.Category.Morphism.IdTransport
import Structure.Category.Morphism.Transport
import Structure.Category.NaturalIsomorphism.Functions
import Structure.Category.NaturalIsomorphism
import Structure.Category.NaturalTransformation.Equiv
import Structure.Category.NaturalTransformation.NaturalTransformations
import Structure.Category.NaturalTransformation
import Structure.Category.On₂
import Structure.Category.Product.Proofs
import Structure.Category.Product.Tuple
import Structure.Category.Product
-- import Structure.Category.Proofs.MonadIsEndofunctorMonoid
import Structure.Category.Proofs
import Structure.Category.Slice
import Structure.Category.Structure.Monoid
import Structure.Category.Tuple.Functors
-- import Structure.Category.Tuple.Proofs.Monoidal
import Structure.Category.Tuple.Proofs
import Structure.Category.Tuple
import Structure.Category
import Structure.Container.IndexedIterable
import Structure.Container.Iterable
import Structure.Container.Map
-- import Structure.Container.SetLike.Proofs
-- import Structure.Container.SetLike
import Structure.Function.Domain.Proofs
import Structure.Function.Domain
import Structure.Function.Linear
import Structure.Function.Metric.Analysis
import Structure.Function.Metric.Proofs
import Structure.Function.Metric.Subspace.Proofs
import Structure.Function.Metric.Subspace.Properties.Proofs
import Structure.Function.Metric.Subspace.Properties
import Structure.Function.Metric.Subspace
import Structure.Function.Metric
import Structure.Function.Multi
import Structure.Function.Names
import Structure.Function.Ordering
import Structure.Function.Proofs
import Structure.Function
import Structure.Groupoid.Functor
import Structure.Groupoid.Groupoids
import Structure.Groupoid
import Structure.IEEE754
import Structure.IndexedCategory.Functor
import Structure.IndexedCategory
import Structure.IndexedOperator.Properties.Preserving
import Structure.IndexedOperator.Properties
import Structure.IndexedOperator
import Structure.IndexedRelator.Properties
import Structure.Logic.Constructive.BoundedPredicate
import Structure.Logic.Constructive.Predicate
import Structure.Logic.Constructive.Proofs
import Structure.Logic.Constructive.Propositional
import Structure.Logic
-- import Structure.Numeral.Integer.Proofs
import Structure.Numeral.Integer
import Structure.Numeral.Natural
import Structure.Operator.Algebra
import Structure.Operator.Field.VectorSpace
import Structure.Operator.Field
import Structure.Operator.Functions
import Structure.Operator.Group.Groups.Trivial
import Structure.Operator.Group.Proofs
import Structure.Operator.Group
import Structure.Operator.IntegralDomain.Proofs
import Structure.Operator.IntegralDomain
import Structure.Operator.InverseOperatorFromFunction.Proofs
import Structure.Operator.InverseOperatorFromFunction
-- import Structure.Operator.Iteration
import Structure.Operator.Lattice.OrderRelation
import Structure.Operator.Lattice
import Structure.Operator.Monoid.Category
import Structure.Operator.Monoid.Homomorphism
import Structure.Operator.Monoid.Invertible.Proofs
import Structure.Operator.Monoid.Invertible
import Structure.Operator.Monoid.Monoids.Coset
import Structure.Operator.Monoid.Monoids.Function
import Structure.Operator.Monoid.Monoids.Trivial
import Structure.Operator.Monoid.Submonoid
import Structure.Operator.Monoid
import Structure.Operator.Names
import Structure.Operator.Proofs.EquivalentStructure
import Structure.Operator.Proofs.ListFoldPermutation
import Structure.Operator.Proofs.Util
import Structure.Operator.Proofs
import Structure.Operator.Properties
import Structure.Operator.Ring.Characteristic.Proofs
import Structure.Operator.Ring.Characteristic
import Structure.Operator.Ring.Homomorphism
import Structure.Operator.Ring.Numerals.Proofs
import Structure.Operator.Ring.Numerals
import Structure.Operator.Ring.Proofs
import Structure.Operator.Ring.Rings.Trivial
import Structure.Operator.Ring
import Structure.Operator.Semi
import Structure.Operator.SetAlgebra
import Structure.Operator.Signature
import Structure.Operator.StarAlgebra
import Structure.Operator.Vector.BilinearOperator
import Structure.Operator.Vector.Eigen
-- import Structure.Operator.Vector.Equiv
import Structure.Operator.Vector.FiniteDimensional.LinearMaps.ChangeOfBasis
-- import Structure.Operator.Vector.FiniteDimensional.Proofs
import Structure.Operator.Vector.FiniteDimensional
import Structure.Operator.Vector.InfiniteDimensional
-- import Structure.Operator.Vector.LinearCombination.Proofs
import Structure.Operator.Vector.LinearCombination
-- import Structure.Operator.Vector.LinearMap.Category
-- import Structure.Operator.Vector.LinearMap.Equiv
import Structure.Operator.Vector.LinearMap
import Structure.Operator.Vector.LinearMaps
import Structure.Operator.Vector.Proofs
-- import Structure.Operator.Vector.Subspace.Proofs
-- import Structure.Operator.Vector.Subspace
-- import Structure.Operator.Vector.Subspaces.DirectSum
-- import Structure.Operator.Vector.Subspaces.Image
-- import Structure.Operator.Vector.Subspaces.Kernel
-- import Structure.Operator.Vector.Subspaces.Span
import Structure.Operator.Vector
import Structure.Operator
import Structure.OrderedField.AbsoluteValue
import Structure.OrderedField.Max
import Structure.OrderedField.Min
import Structure.OrderedField
import Structure.Real.Abs
-- import Structure.Real.Continuity
-- import Structure.Real.Derivative
-- import Structure.Real.Limit
import Structure.Real
import Structure.Relator.Apartness.Proofs
import Structure.Relator.Apartness
import Structure.Relator.Equivalence.Proofs.On₂
import Structure.Relator.Equivalence
import Structure.Relator.Function.Multi
import Structure.Relator.Function.Proofs
import Structure.Relator.Function
import Structure.Relator.Names
import Structure.Relator.Ordering.Lattice.Proofs
import Structure.Relator.Ordering.Lattice
import Structure.Relator.Ordering.Proofs
import Structure.Relator.Ordering
import Structure.Relator.Proofs
import Structure.Relator.Properties.Proofs
import Structure.Relator.Properties
import Structure.Relator
import Structure.Semicategory
import Structure.Set.Equiv
import Structure.Set.Names
import Structure.Set.Operators.Proofs.LogicalOperator
import Structure.Set.Operators
import Structure.Set.Quantifiers.Proofs
import Structure.Set.Quantifiers
import Structure.Set.Relations.Listable
import Structure.Set.Relators.Proofs
import Structure.Set.Relators
import Structure.Set.ZFC.Inductive
import Structure.Set.ZFC.Oper
import Structure.Set.ZFC.Proofs.Classical
import Structure.Set.ZFC
import Structure.Set
import Structure.Setoid.Category.HomFunctor
import Structure.Setoid.Category
import Structure.Setoid.Function
import Structure.Setoid.Names
import Structure.Setoid.On₂
import Structure.Setoid.Proofs
import Structure.Setoid.Signature.IndexedCategory
import Structure.Setoid.Size.Proofs
import Structure.Setoid.Size.Properties.Choice
import Structure.Setoid.Size
-- import Structure.Setoid.Structure.Type.Function
import Structure.Setoid.Uniqueness.Proofs
import Structure.Setoid.Uniqueness
import Structure.Setoid.Universal
import Structure.Setoid
import Structure.Signature
import Structure.SignatureMulti
-- import Structure.Topology.Proofs
-- import Structure.Topology.Properties
import Structure.Topology
import Structure.Type.Dependent.Function.Properties
import Structure.Type.Dependent.Function
-- import Structure.Type.Function.Functions
-- import Structure.Type.Function.Properties
import Structure.Type.Function
import Structure.Type.Identity.Eliminator.Equality.Proofs.Structures
import Structure.Type.Identity.Eliminator.Equality.Proofs
import Structure.Type.Identity.Eliminator.Equality
import Structure.Type.Identity.Eliminator.Functions
import Structure.Type.Identity.GlobalSubstitution.Equality
-- import Structure.Type.Identity.MinimalReflexiveRelation.Equality.Function
import Structure.Type.Identity.MinimalReflexiveRelation.Equality
import Structure.Type.Identity.Proofs
import Structure.Type.Identity
import Structure.Type.Quotient
import Syntax.Do
import Syntax.Existential
import Syntax.Function
import Syntax.Idiom
import Syntax.Implication.Dependent
import Syntax.Implication
import Syntax.List
import Syntax.Number
import Syntax.Transitivity.Structure
import Syntax.Transitivity
import Syntax.Type
import TestProp
-- import Type.Category.Applicative
import Type.Category.FakeExtensionalFunctionsCategory
import Type.Category.Functor
import Type.Category.IntensionalFunctionsCategory
import Type.Category.Monad
import Type.Category
import Type.Cubical.Glue
import Type.Cubical.HTrunc₁
import Type.Cubical.InductiveInterval
import Type.Cubical.InductivePath
import Type.Cubical.Isomorphism.Equiv
import Type.Cubical.Isomorphism.Proofs
import Type.Cubical.Isomorphism
import Type.Cubical.Logic.Extensionality
import Type.Cubical.Logic
import Type.Cubical.Path.Category
import Type.Cubical.Path.Equality
import Type.Cubical.Path.Functions
import Type.Cubical.Path.Proofs
import Type.Cubical.Path.Properties
import Type.Cubical.Path.Univalence
import Type.Cubical.Path
import Type.Cubical.Quotient
import Type.Cubical.Sub
import Type.Cubical.SubtypeSet
import Type.Cubical
import Type.Dependent.Functions
import Type.Dependent.Pi
import Type.Dependent.PiFunction.Category
import Type.Dependent.PiFunction.Equivalence
import Type.Dependent.PiFunction
import Type.Dependent.Sigma.Equiv
import Type.Dependent.Sigma.Functions
import Type.Dependent.Sigma.Implicit
import Type.Dependent.Sigma.Instance
import Type.Dependent.Sigma
import Type.Dependent.Universe
import Type.Identity.Dependent
-- import Type.Identity.Heterogenous.Proofs
-- import Type.Identity.Heterogenous
import Type.Identity.Proofs
import Type.Identity
import Type.Isomorphism.Equiv
import Type.Isomorphism
import Type.M
import Type.Proofs
import Type.Properties.Decidable.Functions
import Type.Properties.Decidable.Proofs
import Type.Properties.Decidable
import Type.Properties.Empty.Proofs
import Type.Properties.Empty
import Type.Properties.Enumerable
-- import Type.Properties.Homotopy.Proofs
import Type.Properties.Homotopy
import Type.Properties.Inhabited
import Type.Properties.Listable
import Type.Properties.MereProposition.Equiv
import Type.Properties.MereProposition.Proofs
import Type.Properties.MereProposition
import Type.Properties.Proofs
import Type.Properties.Singleton.Proofs
import Type.Properties.Singleton
import Type.Singleton.Proofs
import Type.Singleton
import Type.Size.Countable
import Type.Size.Finite
import Type.Size.Proofs
import Type.Size
import Type.Universe
import Type.W.Proofs
import Type.W
import Type
import Typeω.Dependent.Sigma