diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,3 +1,3 @@
 import Distribution.Simple
-main = defaultMain
 
+main = defaultMain
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,3 +1,7 @@
+0.0.5
+
+* Include example of usage of `Presheaf`
+
 0.0.4
 
 * Generalise data types over the Profunctor and not (->)
diff --git a/examples/Data/Valuation/PresheafExample.hs b/examples/Data/Valuation/PresheafExample.hs
new file mode 100644
--- /dev/null
+++ b/examples/Data/Valuation/PresheafExample.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | Take the category with 2 objects 1 and 2 and one arrow between then 1 -> 2 .
+--
+-- This is equivalent to the poset 1 <= 2 .
+--
+-- Take a presheaf that sends 2 to the set of strings {\"cat\"}  and 1  to the set of strings {\"animal\", \"vegetable\"} .
+--
+-- The restriction function is defined so that \"cat\" | 1 = \"animal\"  .
+--
+-- How can we define this in haskell?
+module Data.Valuation.PresheafExample where
+
+import Data.Kind (Type)
+import Data.Semigroupoid (Semigroupoid (..))
+import Data.Valuation.Presheaf (Presheaf (..), runPresheaf)
+
+-- Objects of the category
+data Obj = One | Two deriving (Eq, Show)
+
+-- Morphisms (finite category)
+data Cat :: Obj -> Obj -> Type where
+  Id1 :: Cat 'One 'One
+  Id2 :: Cat 'Two 'Two
+  OneToTwo :: Cat 'One 'Two
+
+instance Semigroupoid Cat where
+  Id1 `o` Id1 = Id1
+  Id2 `o` Id2 = Id2
+  OneToTwo `o` Id1 = OneToTwo
+  Id2 `o` OneToTwo = OneToTwo
+
+-- Values associated with each object
+data OneVal = Animal | Vegetable deriving (Eq, Show)
+
+data TwoVal = Cat deriving (Eq, Show)
+
+-- GADT for the presheaf object mapping
+data F :: Obj -> Type where
+  FOne :: OneVal -> F 'One
+  FTwo :: TwoVal -> F 'Two
+
+-- Example presheaf
+presheafExample :: Presheaf Cat (->) F
+presheafExample = Presheaf go
+  where
+    go :: Cat a b -> F b -> F a
+    -- identities
+    go Id1 x = x
+    go Id2 x = x
+    -- restriction along One -> Two
+    go OneToTwo (FTwo Cat) = FOne Animal
+
+-- Add Show instance for F
+instance Show (F 'One) where
+  show (FOne x) = show x
+
+instance Show (F 'Two) where
+  show (FTwo x) = show x
+
+-- Example usage
+example :: F 'One
+example = runPresheaf presheafExample OneToTwo (FTwo Cat)
diff --git a/src/Data/Valuation.hs b/src/Data/Valuation.hs
--- a/src/Data/Valuation.hs
+++ b/src/Data/Valuation.hs
@@ -115,7 +115,7 @@
 --
 -- === Presheaf
 --
--- A reified presheaf: 'Presheaf' @cat f cat'@ wraps @forall a b. cat a b -> cat' (f b) (f a)@, representing a contravariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is exactly 'Data.Functor.Contravariant.contramap'. Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Contravariant.Predicate', 'Data.Functor.Contravariant.Comparison', 'Data.Functor.Contravariant.Equivalence', 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@).
+-- A reified presheaf: 'Presheaf' @cat f cat'@ wraps @forall a b. cat a b -> cat' (f b) (f a)@, representing a contravariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is exactly 'Data.Functor.Contravariant.contramap'. Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Contravariant.Predicate', 'Data.Functor.Contravariant.Comparison', 'Data.Functor.Contravariant.Equivalence', 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@). For a worked example of defining a 'Presheaf' over a finite category, see "Data.Valuation.PresheafExample".
 --
 -- === CovariantFunctor
 --
@@ -204,6 +204,7 @@
 -- * "Data.Valuation.Valuation" — Domain-information pairs
 -- * "Data.Valuation.ValuationAlgebra" — Full algebra with unit and zero
 -- * "Data.Valuation.ValuationAlgebraOp" — Operations on valuation algebras (@set var -> v@)
+-- * "Data.Valuation.PresheafExample" — Worked example: a presheaf over a finite category
 module Data.Valuation
   ( module V,
   )
diff --git a/src/Data/Valuation/Presheaf.hs b/src/Data/Valuation/Presheaf.hs
--- a/src/Data/Valuation/Presheaf.hs
+++ b/src/Data/Valuation/Presheaf.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# OPTIONS_GHC -Wall -Werror #-}
 
@@ -18,6 +19,9 @@
 -- newtype 'Presheaf' cat cat' f = 'Presheaf' (forall a b. cat a b -> cat' (f b) (f a))
 -- type 'Presheaf'' f = 'Presheaf' (->) (->) f
 -- @
+--
+-- For a worked example of defining a 'Presheaf' over a finite category,
+-- see "Data.Valuation.PresheafExample".
 module Data.Valuation.Presheaf
   ( Presheaf (..),
     Presheaf',
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -6,10 +6,13 @@
 import System.Process (rawSystem)
 
 main :: IO ()
-main = exitWith =<< rawSystem "cabal"
-  [ "repl"
-  , "--with-compiler=doctest"
-  , "--repl-options=-w"
-  , "--repl-options=-Wdefault"
-  , "lib:valuations"
-  ]
+main =
+  exitWith
+    =<< rawSystem
+      "cabal"
+      [ "repl",
+        "--with-compiler=doctest",
+        "--repl-options=-w",
+        "--repl-options=-Wdefault",
+        "lib:valuations"
+      ]
diff --git a/valuations.cabal b/valuations.cabal
--- a/valuations.cabal
+++ b/valuations.cabal
@@ -1,6 +1,6 @@
 cabal-version:        2.4
 name:                 valuations
-version:              0.0.4
+version:              0.0.5
 synopsis:             Valuations
 description:          Valuations: Valuation and Valuation Algebra
 license:              BSD-3-Clause
@@ -35,6 +35,8 @@
                       Data.Valuation.ValuationAlgebra
                       Data.Valuation.ValuationAlgebraOp
 
+                      Data.Valuation.PresheafExample
+
   build-depends:        base >= 4.8 && < 6
                       , adjunctions >= 4.4 && < 5
                       , bifunctors >= 5 && < 6
@@ -50,6 +52,7 @@
                       , witherable >= 0.4 && < 1
 
   hs-source-dirs:     src
+                      examples
 
   default-language:   Haskell2010