remove spaces

src/Free/FreeFunctor.lidr

@@ -20,29 +20,29 @@ 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)
 >   -> Path g i j
 >   -> 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)

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

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)

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)