module Everything where

import Prelude.Category
import Prelude.Category.Isomorphism
import Prelude.Category.Isomorphism.Functor
import Prelude.Category.NaturalTransformation
import Prelude.Category.Pullback
import Prelude.Category.Pullback.Midpoint
import Prelude.Category.Slice
import Prelude.Category.Slice.Functor
import Prelude.Category.Span
import Prelude.Category.WCat
import Prelude.Equality
import Prelude.Function
import Prelude.Function.Fam
import Prelude.Function.Isomorphism
import Prelude.InverseImage
import Prelude.Preorder
import Prelude.Product
import Refinement
import Refinement.Category
import Description
import Description.Horizontal
import Ornament
import Ornament.Algebraic
import Ornament.Algebraic.EquivalenceTheorem
import Ornament.Category
import Ornament.Equivalence
import Ornament.Horizontal
import Ornament.Horizontal.Category
import Ornament.Horizontal.Equivalence
import Ornament.Horizontal.Pullback
import Ornament.ParallelComposition
import Ornament.ParallelComposition.Pullback
import Ornament.ParallelComposition.Swap
import Ornament.RefinementSemantics
import Ornament.SequentialComposition
import Relation
import Relation.AlgCategory
import Relation.CompChain
import Relation.Division
import Relation.Fold
import Relation.GreedyTheorem
import Relation.Hylomorphism
import Relation.Join
import Relation.Meet
import Relation.Minimum
import Examples.BinomialHeap
import Examples.Bool
import Examples.Fin
import Examples.FoldFusion
import Examples.Insertion
import Examples.LeftistHeap
import Examples.List
import Examples.List.Ordered
import Examples.List.Vec
import Examples.Metamorphism
import Examples.MinCoinChange
import Examples.Nat
import Examples.Nat.TotalOrdering