module Main where
open import Chapter2.Logic
open import Chapter2.IProp
open import Chapter2.Equality
open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint
open import Chapter4.Desc.InitialAlgebra
open import Chapter4.Desc.Lifting
open import Chapter4.Desc.Induction
open import Chapter4.Desc.Tagged
open import Chapter4.Desc.Examples.Main
open import Chapter4.Desc.Examples.Nat
open import Chapter4.Desc.Examples.List
open import Chapter4.Desc.Examples.Tree
open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra
open import Chapter5.IDesc.Lifting
open import Chapter5.IDesc.Induction
open import Chapter5.IDesc.Tagged
open import Chapter5.IDesc.Examples.Main
open import Chapter5.IDesc.Examples.ToIDesc
open import Chapter5.IDesc.Examples.Bool
open import Chapter5.IDesc.Examples.Nat
open import Chapter5.IDesc.Examples.Forest
open import Chapter5.IDesc.Examples.Vec
open import Chapter5.IDesc.Examples.Fin
open import Chapter5.IDesc.Examples.Walk
open import Chapter5.IDesc.Examples.Expr
open import Chapter5.Container
open import Chapter5.Container.Morphism
open import Chapter5.Container.Examples.Main
open import Chapter5.Container.Examples.Nat
open import Chapter5.Container.Examples.List
open import Chapter5.Container.Examples.Vec
open import Chapter5.IDesc.Algebra.Main
open import Chapter5.IDesc.Algebra.Quantifiers
open import Chapter5.IDesc.Algebra.Composition
open import Chapter5.Equivalence.ToContainer
open import Chapter5.Equivalence.ToDesc
open import Chapter6.EnumU
open import Chapter6.EnumU.Pi
open import Chapter6.Desc
open import Chapter6.Desc.Levitation
open import Chapter6.Desc.InitialAlgebra
open import Chapter6.Desc.FreeMonad
open import Chapter6.Desc.FreeMonad.Monad
open import Chapter6.Desc.FreeMonad.Examples.List
open import Chapter6.Desc.FreeMonad.Examples.TermIO
open import Chapter6.IDesc
open import Chapter6.IDesc.Levitation
open import Chapter6.IDesc.InitialAlgebra
open import Chapter6.IDesc.FreeMonad
open import Chapter6.IDesc.FreeMonad.Monad
open import Chapter6.IDesc.FreeMonad.Examples.FileSystem
open import Chapter6.IDesc.FreeMonad.Examples.IDesc
open import Chapter6.IDesc.Examples.Expr
open import Chapter6.Universe
open import Chapter7.Case
open import Chapter7.NoConfusion
open import Chapter7.Derivable
open import Chapter7.Derivable.Equality
open import Chapter7.Derivable.Examples.Nat
open import Chapter8.Ornament
open import Chapter8.Ornament.CartesianMorphism
open import Chapter8.Ornament.Algebra
open import Chapter8.Ornament.Identity
open import Chapter8.Ornament.Examples.Maybe
open import Chapter8.Ornament.Examples.List
open import Chapter8.Ornament.Examples.Fin
open import Chapter8.Ornament.Examples.Vec
open import Chapter8.Ornament.Examples.Lifting
open import Chapter8.AlgebraicOrnament
open import Chapter8.AlgebraicOrnament.Coherence
open import Chapter8.AlgebraicOrnament.Make
open import Chapter8.AlgebraicOrnament.Examples.Interval
open import Chapter8.AlgebraicOrnament.Examples.Expr
open import Chapter8.AlgebraicOrnament.Examples.Vec
open import Chapter8.AlgebraicOrnament.Examples.Lifting
open import Chapter8.Reornament
open import Chapter8.Reornament.Coherence
open import Chapter8.Reornament.Make
open import Chapter8.Reornament.Examples.List
open import Chapter8.Reornament.Examples.Maybe
open import Chapter8.Brady.Main
open import Chapter8.Brady.Vec
open import Chapter8.Brady.Fin
open import Chapter8.Container.BaseChange
open import Chapter8.Container.CobaseChange
open import Chapter8.Container.Morphism.Main
open import Chapter8.Container.Morphism.Cartesian
open import Chapter8.Container.Morphism.Contornament
open import Chapter8.Container.Morphism.Examples.List
open import Chapter8.Equivalence.Main
open import Chapter8.Equivalence.ToContornament
open import Chapter8.Equivalence.ToCartesian
open import Chapter8.Equivalence.ToOrn
open import Chapter8.Container.Morphism.Cartesian.Main
open import Chapter8.Container.Morphism.Cartesian.Identity
open import Chapter8.Container.Morphism.Cartesian.Composition.Vertical
open import Chapter8.Container.Morphism.Contornament.Main
open import Chapter8.Container.Morphism.Contornament.Identity
open import Chapter8.Container.Morphism.Contornament.Composition.Vertical
open import Chapter8.Container.Morphism.Contornament.Composition.Horizontal
open import Chapter8.Container.Morphism.Contornament.Pullback
open import Chapter9.Example
open import Chapter9.Functions
open import Chapter9.Functions.Examples.Le
open import Chapter9.Functions.Examples.Plus
open import Chapter9.FunOrnament
open import Chapter9.FunOrnament.Examples.Lookup
open import Chapter9.FunOrnament.Examples.Append
open import Chapter9.Patch
open import Chapter9.Patch.Apply
open import Chapter9.Patch.Coherence
open import Chapter9.Patch.Examples.Lookup
open import Chapter9.Patch.Examples.Append
open import Chapter9.Lift.Main
open import Chapter9.Lift.Fold
open import Chapter9.Lift.Induction
open import Chapter9.Lift.Case
open import Chapter9.Lift.Constructor
open import Chapter9.Lift.Examples.Head
open import Chapter9.Lift.Examples.Lookup
open import Chapter9.Lift.Examples.Append