generalize graphs, rename old def to finite graph

.gitignore

@@ -22,3 +22,5 @@ target
 elba.lock
 build
 compare
+*.ttc
+*.ttm

idris-ct.ipkg

@@ -45,6 +45,10 @@ modules =
   Dual.DualFunctor,
   Empty.EmptyCategory,
   Empty.EmptyFunctor,
+  Free.Finite.FinGraph,
+  Free.Finite.FinPath,
+  Free.Finite.FinPathCategory,
+  Free.Finite.FreeFinFunctor,
   Free.FreeFunctor,
   Free.Graph,
   Free.Path,

src/Free/Finite/FinGraph.lidr

@@ -0,0 +1,46 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Free.Finite.FinGraph
+>
+> import Data.Vect
+>
+> %access public export
+> %default total
+>
+> record FinGraph where
+>   constructor MkFinGraph
+>   vertices : Type
+>   edges    : Vect n (vertices, vertices)
+>
+> Edge : (g : FinGraph) -> (i, j : vertices g) -> Type
+> Edge g i j = Elem (i, j) (edges g)
+>
+> edgeOrigin : {g : FinGraph} -> Edge g i j -> vertices g
+> edgeOrigin {i} _ = i
+>
+> edgeTarget : {g : FinGraph} -> Edge g i j -> vertices g
+> edgeTarget {j} _ = j
+
+data TriangleVertices = One | Two | Three
+
+triangle : FinGraph
+triangle = MkFinGraph TriangleVertices [(One, Two), (Two, Three), (Three, One)]

src/Free/Finite/FinPath.lidr

@@ -0,0 +1,60 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Free.Finite.FinPath
+>
+> import Data.List
+> import Free.Finite.FinGraph
+>
+> %access public export
+> %default total
+>
+> data FinPath : (g : FinGraph) -> vertices g -> vertices g -> Type where
+>   Nil  : FinPath g i i
+>   (::) : (a : Edge g i j) -> FinPath g j k -> FinPath g i k
+
+nullFinPath : FinPath FinGraph.triangle One One
+nullFinPath = Nil
+
+oneToThree : FinPath FinGraph.triangle One Three
+oneToThree = [Here, There Here]
+
+oneToThree' : FinPath FinGraph.triangle One Three
+oneToThree' = Here :: There Here :: Nil
+
+> edgeToFinPath : {g : FinGraph} -> (a : Edge g i j) -> FinPath g (edgeOrigin a) (edgeTarget a)
+> edgeToFinPath a = [a]
+>
+> joinFinPath : FinPath g i j -> FinPath g j k -> FinPath g i k
+> joinFinPath [] y = y
+> joinFinPath (x :: xs) y = x :: joinFinPath xs y
+>
+> joinFinPathNil : (p : FinPath g i j) -> joinFinPath p [] = p
+> joinFinPathNil Nil       = Refl
+> joinFinPathNil (x :: xs) = cong $ joinFinPathNil xs
+>
+> joinFinPathAssoc :
+>      (p : FinPath g i j)
+>   -> (q : FinPath g j k)
+>   -> (r : FinPath g k l)
+>   -> joinFinPath p (joinFinPath q r) = joinFinPath (joinFinPath p q) r
+> joinFinPathAssoc Nil q r = Refl
+> joinFinPathAssoc (x :: xs) q r = cong $ joinFinPathAssoc xs q r

src/Free/Finite/FinPathCategory.lidr

@@ -0,0 +1,40 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Free.Finite.FinPathCategory
+>
+> import Basic.Category
+> import Data.Vect
+> import Free.FinGraph
+> import Free.FinPath
+>
+> %access public export
+> %default total
+>
+> pathCategory : FinGraph -> Category
+> pathCategory g = MkCategory
+>   (vertices g)
+>   (FinPath g)
+>   (\a => Nil)
+>   (\a, b, c, f, g => joinFinPath f g)
+>   (\a, b, f => Refl)
+>   (\a, b, f => joinFinPathNil f)
+>   (\a, b, c, d, f, g, h => joinFinPathAssoc f g h)

src/Free/Finite/FreeFinFunctor.lidr

@@ -0,0 +1,73 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Free.Finite.FreeFinFunctor
+>
+> import Basic.Category
+> import Basic.Functor
+> import Data.Vect
+> import Free.Finite.FinGraph
+> import Free.Finite.FinPath
+> import Free.Finite.FinPathCategory
+>
+> %access public export
+> %default total
+>
+> record FinGraphEmbedding (g : FinGraph) (cat : Category) where
+>   constructor MkFinGraphEmbedding
+>   mapVertices : vertices g -> obj cat
+>   mapEdges    : (i, j : vertices g) -> Edge g i j -> mor cat (mapVertices i) (mapVertices j)
+>
+> foldFinPath :
+>      (g : FinGraph)
+>   -> (ge : FinGraphEmbedding g cat)
+>   -> FinPath g i j
+>   -> mor cat (mapVertices ge i) (mapVertices ge j)
+> foldFinPath _ {cat} ge {i} []              = identity cat (mapVertices ge i)
+> foldFinPath g {cat} ge {i} ((::) {j} x xs) = compose cat _ _ _ (mapEdges ge i j x) (foldFinPath g ge xs)
+>
+> freeFinFunctorCompose :
+>      (g : FinGraph)
+>   -> (ge : FinGraphEmbedding g cat)
+>   -> (i, j, k : vertices g)
+>   -> (f : FinPath g i j)
+>   -> (h : FinPath g j k)
+>   -> foldFinPath g ge {i} {j = k} (joinFinPath f h)
+>    = compose cat
+>              (mapVertices ge i)
+>              (mapVertices ge j)
+>              (mapVertices ge k)
+>              (foldFinPath g ge {i} {j} f)
+>              (foldFinPath g ge {i = j} {j = k} h)
+> freeFinFunctorCompose g {cat} ge j j k [] h = sym $ leftIdentity cat
+>                                                               (mapVertices ge j)
+>                                                               (mapVertices ge k)
+>                                                               (foldFinPath g ge h)
+> freeFinFunctorCompose g {cat} ge i j k ((::) {j=l} x xs) h =
+>   trans (cong {f = compose cat _ _ _ (mapEdges ge i l x)} $ freeFinFunctorCompose g ge _ _ _ xs h)
+>         (associativity cat _ _ _ _ (mapEdges ge i l x) (foldFinPath g ge xs) (foldFinPath g ge h))
+>
+> freeFinFunctor : (g : FinGraph) -> FinGraphEmbedding g cat -> CFunctor (pathCategory g) cat
+> freeFinFunctor g ge = MkCFunctor
+>   (mapVertices ge)
+>   (\i, j, p => foldFinPath g ge {i} {j} p)
+>   (\_ => Refl)
+>   (freeFinFunctorCompose g ge)

src/Free/FreeFunctor.lidr

@@ -20,30 +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 Data.Vect
 > 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) -> Edge g i j -> mor cat (mapVertices i) (mapVertices j)
->
+>   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)
@@ -64,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,27 +20,11 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 \fi
 
 > module Free.Graph
->
-> import Data.Vect
->
+> 
 > %access public export
 > %default total
->
+> 
 > record Graph where
 >   constructor MkGraph
 >   vertices : Type
->   edges    : Vect n (vertices, vertices)
->
-> Edge : (g : Graph) -> (i, j : vertices g) -> Type
-> Edge g i j = Elem (i, j) (edges g)
->
-> edgeOrigin : {g : Graph} -> Edge g i j -> vertices g
-> edgeOrigin {i} _ = i
->
-> edgeTarget : {g : Graph} -> Edge g i j -> vertices g
-> edgeTarget {j} _ = j
-
-data TriangleVertices = One | Two | Three
-
-triangle : Graph
-triangle = MkGraph TriangleVertices [(One, Two), (Two, Three), (Three, One)]
+>   edges    : vertices -> vertices -> Type

src/Free/Path.lidr

@@ -20,37 +20,27 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 \fi
 
 > module Free.Path
->
-> import Data.List
+> 
 > import Free.Graph
->
+> 
 > %access public export
 > %default total
->
+> 
 > data Path : (g : Graph) -> vertices g -> vertices g -> Type where
 >   Nil  : Path g i i
->   (::) : (a : Edge g i j) -> Path g j k -> Path g i k
-
-nullPath : Path Graph.triangle One One
-nullPath = Nil
-
-oneToThree : Path Graph.triangle One Three
-oneToThree = [Here, There Here]
-
-oneToThree' : Path Graph.triangle One Three
-oneToThree' = Here :: There Here :: Nil
-
-> edgeToPath : {g : Graph} -> (a : Edge g i j) -> Path g (edgeOrigin a) (edgeTarget a)
-> edgeToPath a = [a]
+>   (::) : 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)