module Readme where -- This file implements the definitions and examples provided in the -- paper. It is known to type-check with Agda version 2.4.3. -- * Signature open import Signature -- ** Examples open import Signature.Vector open import Signature.Nat open import Signature.List open import Signature.Fin open import Signature.Tree -- * (Naive) ornaments open import Ornament -- ** Examples open import Ornament.List open import Ornament.Fin -- * Cartesian morphism open import Cartesian open import Cartesian.Translation -- ** Examples open import Cartesian.List -- * Structure open import Structure.OrnamentalAlgebra open import Structure.Composition