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