From 60108d3ff920f9ff18883672a5e370d6ec95997a Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 29 Aug 2019 21:31:35 +0300 Subject: [PATCH] generalize graphs, rename old def to finite graph --- .gitignore | 2 + idris-ct.ipkg | 4 ++ src/Free/Finite/FinGraph.lidr | 46 ++++++++++++++++++ src/Free/Finite/FinPath.lidr | 60 +++++++++++++++++++++++ src/Free/Finite/FinPathCategory.lidr | 40 +++++++++++++++ src/Free/Finite/FreeFinFunctor.lidr | 73 ++++++++++++++++++++++++++++ src/Free/FreeFunctor.lidr | 15 +++--- src/Free/Graph.lidr | 22 ++------- src/Free/Path.lidr | 28 ++++------- src/Free/PathCategory.lidr | 6 +-- 10 files changed, 247 insertions(+), 49 deletions(-) create mode 100644 src/Free/Finite/FinGraph.lidr create mode 100644 src/Free/Finite/FinPath.lidr create mode 100644 src/Free/Finite/FinPathCategory.lidr create mode 100644 src/Free/Finite/FreeFinFunctor.lidr diff --git a/.gitignore b/.gitignore index 33c23bc..61fab51 100644 --- a/.gitignore +++ b/.gitignore @@ -22,3 +22,5 @@ target elba.lock build compare +*.ttc +*.ttm diff --git a/idris-ct.ipkg b/idris-ct.ipkg index b1e9a07..0e308fb 100644 --- a/idris-ct.ipkg +++ b/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, diff --git a/src/Free/Finite/FinGraph.lidr b/src/Free/Finite/FinGraph.lidr new file mode 100644 index 0000000..9baae2f --- /dev/null +++ b/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 + +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 . +\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)] diff --git a/src/Free/Finite/FinPath.lidr b/src/Free/Finite/FinPath.lidr new file mode 100644 index 0000000..958a041 --- /dev/null +++ b/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 + +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 . +\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 diff --git a/src/Free/Finite/FinPathCategory.lidr b/src/Free/Finite/FinPathCategory.lidr new file mode 100644 index 0000000..095e826 --- /dev/null +++ b/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 + +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 . +\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) diff --git a/src/Free/Finite/FreeFinFunctor.lidr b/src/Free/Finite/FreeFinFunctor.lidr new file mode 100644 index 0000000..0266192 --- /dev/null +++ b/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 + +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 . +\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) diff --git a/src/Free/FreeFunctor.lidr b/src/Free/FreeFunctor.lidr index b695de4..0c616e0 100644 --- a/src/Free/FreeFunctor.lidr +++ b/src/Free/FreeFunctor.lidr @@ -20,22 +20,21 @@ along with this program. If not, see . \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) @@ -43,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) @@ -64,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 5bc70b2..578b622 100644 --- a/src/Free/Graph.lidr +++ b/src/Free/Graph.lidr @@ -20,27 +20,11 @@ along with this program. If not, see . \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 diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr index 763c666..12a1fa0 100644 --- a/src/Free/Path.lidr +++ b/src/Free/Path.lidr @@ -20,37 +20,27 @@ along with this program. If not, see . \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) diff --git a/src/Free/PathCategory.lidr b/src/Free/PathCategory.lidr index 6c89f0d..740ecc7 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)