From 5a8944d27e0ee684ac47729f5c2f975f6aa20030 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Thu, 29 Aug 2019 21:34:55 +0300
Subject: [PATCH] remove spaces

---
 src/Free/FreeFunctor.lidr  | 12 ++++++------
 src/Free/Graph.lidr        |  4 ++--
 src/Free/Path.lidr         | 12 ++++++------
 src/Free/PathCategory.lidr |  6 +++---
 4 files changed, 17 insertions(+), 17 deletions(-)

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 <https://www.gnu.org/licenses/>.
 \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 <https://www.gnu.org/licenses/>.
 >   -> 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 <https://www.gnu.org/licenses/>.
 > 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 <https://www.gnu.org/licenses/>.
 \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 <https://www.gnu.org/licenses/>.
 \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 <https://www.gnu.org/licenses/>.
 \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)