diff --git a/src/Free/FreeFunctor.lidr b/src/Free/FreeFunctor.lidr
index 0c616e0..c29a830 100644
--- a/src/Free/FreeFunctor.lidr
+++ b/src/Free/FreeFunctor.lidr
@@ -20,21 +20,21 @@ along with this program. If not, see .
\fi
> module Free.FreeFunctor
->
+>
> import Basic.Category
> import Basic.Functor
> import Free.Graph
> import Free.Path
> import Free.PathCategory
->
+>
> %access public export
> %default total
->
+>
> record GraphEmbedding (g : Graph) (cat : Category) where
> constructor MkGraphEmbedding
> mapVertices : vertices g -> obj cat
> mapEdges : (i, j : vertices g) -> edges g i j -> mor cat (mapVertices i) (mapVertices j)
->
+>
> foldPath :
> (g : Graph)
> -> (ge : GraphEmbedding g cat)
@@ -42,7 +42,7 @@ along with this program. If not, see .
> -> mor cat (mapVertices ge i) (mapVertices ge j)
> foldPath _ {cat} ge {i} [] = identity cat (mapVertices ge i)
> foldPath g {cat} ge {i} ((::) {j} x xs) = compose cat _ _ _ (mapEdges ge i j x) (foldPath g ge xs)
->
+>
> freeFunctorCompose :
> (g : Graph)
> -> (ge : GraphEmbedding g cat)
@@ -63,7 +63,7 @@ along with this program. If not, see .
> freeFunctorCompose g {cat} ge i j k ((::) {j=l} x xs) h =
> trans (cong {f = compose cat _ _ _ (mapEdges ge i l x)} $ freeFunctorCompose g ge _ _ _ xs h)
> (associativity cat _ _ _ _ (mapEdges ge i l x) (foldPath g ge xs) (foldPath g ge h))
->
+>
> freeFunctor : (g : Graph) -> GraphEmbedding g cat -> CFunctor (pathCategory g) cat
> freeFunctor g ge = MkCFunctor
> (mapVertices ge)
diff --git a/src/Free/Graph.lidr b/src/Free/Graph.lidr
index 578b622..5105ec4 100644
--- a/src/Free/Graph.lidr
+++ b/src/Free/Graph.lidr
@@ -20,10 +20,10 @@ along with this program. If not, see .
\fi
> module Free.Graph
->
+>
> %access public export
> %default total
->
+>
> record Graph where
> constructor MkGraph
> vertices : Type
diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr
index 12a1fa0..e5997ef 100644
--- a/src/Free/Path.lidr
+++ b/src/Free/Path.lidr
@@ -20,27 +20,27 @@ along with this program. If not, see .
\fi
> module Free.Path
->
+>
> import Free.Graph
->
+>
> %access public export
> %default total
->
+>
> data Path : (g : Graph) -> vertices g -> vertices g -> Type where
> Nil : Path g i i
> (::) : edges g i j -> Path g j k -> Path g i k
>
> edgeToPath : {g : Graph} -> edges g i j -> Path g i j
> edgeToPath a = [a]
->
+>
> joinPath : Path g i j -> Path g j k -> Path g i k
> joinPath [] y = y
> joinPath (x :: xs) y = x :: joinPath xs y
->
+>
> joinPathNil : (p : Path g i j) -> joinPath p [] = p
> joinPathNil Nil = Refl
> joinPathNil (x :: xs) = cong $ joinPathNil xs
->
+>
> joinPathAssoc :
> (p : Path g i j)
> -> (q : Path g j k)
diff --git a/src/Free/PathCategory.lidr b/src/Free/PathCategory.lidr
index 740ecc7..6c89f0d 100644
--- a/src/Free/PathCategory.lidr
+++ b/src/Free/PathCategory.lidr
@@ -20,15 +20,15 @@ along with this program. If not, see .
\fi
> module Free.PathCategory
->
+>
> import Basic.Category
> import Data.Vect
> import Free.Graph
> import Free.Path
->
+>
> %access public export
> %default total
->
+>
> pathCategory : Graph -> Category
> pathCategory g = MkCategory
> (vertices g)