From 60108d3ff920f9ff18883672a5e370d6ec95997a Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 29 Aug 2019 21:31:35 +0300 Subject: [PATCH 01/15] 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) From b2dbd81c249c7ce2af31566a354991b856271516 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 29 Aug 2019 21:34:55 +0300 Subject: [PATCH 02/15] 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 . \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) From 3a7f0168f692e8b621d20c666ac8e6c3b80ef09d Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Fri, 30 Aug 2019 13:44:02 +0300 Subject: [PATCH 03/15] fix imports --- src/Free/Finite/FinPathCategory.lidr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Free/Finite/FinPathCategory.lidr b/src/Free/Finite/FinPathCategory.lidr index 095e826..4386c5d 100644 --- a/src/Free/Finite/FinPathCategory.lidr +++ b/src/Free/Finite/FinPathCategory.lidr @@ -23,8 +23,8 @@ along with this program. If not, see . > > import Basic.Category > import Data.Vect -> import Free.FinGraph -> import Free.FinPath +> import Free.Finite.FinGraph +> import Free.Finite.FinPath > > %access public export > %default total From fca499f51fa69c9d21f4474fe3e01477bf0d3641 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Wed, 6 Nov 2019 18:10:51 +0100 Subject: [PATCH 04/15] remove trailing white space --- idris2/Free/Graph.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/idris2/Free/Graph.idr b/idris2/Free/Graph.idr index f389360..839fbb0 100644 --- a/idris2/Free/Graph.idr +++ b/idris2/Free/Graph.idr @@ -22,6 +22,6 @@ edgeTarget : {0 i : vertices g} -> {j : vertices g} -> Edge g i j -> vertices g edgeTarget _ = j -- data TriangleVertices = One | Two | Three --- +-- -- triangle : Graph -- triangle = MkGraph TriangleVertices [(One, Two), (Two, Three), (Three, One)] From fd01c7b1e4ed0472bdc0ec3a8423b78ccd8705a9 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Wed, 6 Nov 2019 18:11:53 +0100 Subject: [PATCH 05/15] provide edgeList Graph constructor --- src/Free/Graph.lidr | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Free/Graph.lidr b/src/Free/Graph.lidr index 5105ec4..0334a76 100644 --- a/src/Free/Graph.lidr +++ b/src/Free/Graph.lidr @@ -21,6 +21,8 @@ along with this program. If not, see . > module Free.Graph > +> import Data.Vect +> > %access public export > %default total > @@ -28,3 +30,10 @@ along with this program. If not, see . > constructor MkGraph > vertices : Type > edges : vertices -> vertices -> Type +> +> edgeList : Eq vertices +> => (edges : Vect n (vertices, vertices)) +> -> Graph +> edgeList edges = MkGraph +> vertices +> (\v1, v2 => Fin $ fst $ filter ((==) (v1, v2)) edges) From a2dee9a6110a9484960fae731b0c1ac438a5301d Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Thu, 7 Nov 2019 15:38:41 +0100 Subject: [PATCH 06/15] adapt pushout to new graph definition --- src/CoLimits/Pushout.lidr | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/CoLimits/Pushout.lidr b/src/CoLimits/Pushout.lidr index 4d59245..f134b23 100644 --- a/src/CoLimits/Pushout.lidr +++ b/src/CoLimits/Pushout.lidr @@ -33,10 +33,14 @@ along with this program. If not, see . > > data PushoutIndexObject = X | Y | Z > +> Eq PushoutIndexObject where +> X == X = True +> Y == Y = True +> Z == Z = True +> _ == _ = False +> > PushoutIndexGraph : Graph -> PushoutIndexGraph = MkGraph -> PushoutIndexObject -> [(Z, X), (Z, Y)] +> PushoutIndexGraph = edgeList [(Z, X), (Z, Y)] > > PushoutIndexCategory : Category > PushoutIndexCategory = pathCategory PushoutIndexGraph From 3c14ddfda745d7f75c9e3108da63029741ec836e Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Thu, 7 Nov 2019 19:20:22 +0100 Subject: [PATCH 07/15] decidable filter on edgeList --- src/Free/Graph.lidr | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Free/Graph.lidr b/src/Free/Graph.lidr index 0334a76..59a6602 100644 --- a/src/Free/Graph.lidr +++ b/src/Free/Graph.lidr @@ -31,9 +31,15 @@ along with this program. If not, see . > vertices : Type > edges : vertices -> vertices -> Type > -> edgeList : Eq vertices +> decidableFilter : DecEq a => (v : a) -> Vect n a -> (k ** Vect k (e ** e = v)) +> decidableFilter v [] = (0 ** []) +> decidableFilter v (x :: xs) with (decEq x v) +> decidableFilter v (x :: xs) | Yes prf = let (i ** vs) = decidableFilter v xs in (S i ** (x ** prf) :: vs) +> decidableFilter v (x :: xs) | No cont = decidableFilter v xs +> +> edgeList : DecEq vertices > => (edges : Vect n (vertices, vertices)) > -> Graph > edgeList edges = MkGraph > vertices -> (\v1, v2 => Fin $ fst $ filter ((==) (v1, v2)) edges) +> (\v1, v2 => Fin $ DPair.fst $ decidableFilter (v1, v2) edges) From 85c45733b766e7aeb1b8a44e93f22356c5e162c0 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Thu, 7 Nov 2019 19:21:08 +0100 Subject: [PATCH 08/15] progress on build a path from an edge list --- src/Free/Path.lidr | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr index e5997ef..c7defb6 100644 --- a/src/Free/Path.lidr +++ b/src/Free/Path.lidr @@ -21,6 +21,7 @@ along with this program. If not, see . > module Free.Path > +> import Data.Vect > import Free.Graph > > %access public export @@ -48,3 +49,24 @@ along with this program. If not, see . > -> joinPath p (joinPath q r) = joinPath (joinPath p q) r > joinPathAssoc Nil q r = Refl > joinPathAssoc (x :: xs) q r = cong $ joinPathAssoc xs q r +> +> data EdgeListPath : (edges : Vect n (vertices, vertices)) -> vertices -> vertices -> Type where +> Empty : EdgeListPath edges i i +> Cons : Elem (i, j) edges -> EdgeListPath edges j k -> EdgeListPath edges i k +> +> +> filterElemWhichIsHere : Eq t => (x : t) -> (l : Vect _ t) -> (k : Nat ** DPair.fst $ filter ((==) x) (x :: l) = S k) +> filterElemWhichIsHere x [] = (0 ** ?asdf) +> filterElemWhichIsHere x xs = ?qwer +> +> -- countOccurence : Eq vertices => {v1, v2 : vertices} -> Elem (v1, v2) edges -> Fin $ fst $ filter ((==) (v1, v2)) edges +> -- countOccurence {edges = (v1 , v2 ) :: l} Here = rewrite DPair.snd $ filterElemWhichIsHere l (v1, v2) in 0 +> -- countOccurence {v1} {v2} {edges = (v1', v2') :: l} (There a) = let rec = countOccurence a in if (v1', v2') == (v1,v2) then weaken rec else ?qwer +> +> -- edgeListPath : Eq vertices +> -- => {edges : Vect n (vertices, vertices)} +> -- -> {i, j : vertices} +> -- -> EdgeListPath edges i j +> -- -> Path (edgeList edges) i j +> -- edgeListPath Empty = Nil +> -- edgeListPath (Cons elem elp) = (countOccurence {edges} elem) :: (edgeListPath elp) From 7d61a70e727a93dd8a98d002cd6a519ea539ae2f Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 12 Nov 2019 09:37:34 +0100 Subject: [PATCH 09/15] implement edgeList with decEqFilter --- src/Free/Graph.lidr | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Free/Graph.lidr b/src/Free/Graph.lidr index 59a6602..2a6b244 100644 --- a/src/Free/Graph.lidr +++ b/src/Free/Graph.lidr @@ -31,15 +31,15 @@ along with this program. If not, see . > vertices : Type > edges : vertices -> vertices -> Type > -> decidableFilter : DecEq a => (v : a) -> Vect n a -> (k ** Vect k (e ** e = v)) -> decidableFilter v [] = (0 ** []) -> decidableFilter v (x :: xs) with (decEq x v) -> decidableFilter v (x :: xs) | Yes prf = let (i ** vs) = decidableFilter v xs in (S i ** (x ** prf) :: vs) -> decidableFilter v (x :: xs) | No cont = decidableFilter v xs +> decEqFilter : DecEq a => (v : a) -> Vect n a -> (k ** Vect k (e ** e = v)) +> decEqFilter v [] = (0 ** []) +> decEqFilter v (x :: xs) with (decEq x v) +> decEqFilter v (x :: xs) | Yes prf = let (i ** vs) = decEqFilter v xs in (S i ** (x ** prf) :: vs) +> decEqFilter v (x :: xs) | No cont = decEqFilter v xs > > edgeList : DecEq vertices > => (edges : Vect n (vertices, vertices)) > -> Graph > edgeList edges = MkGraph > vertices -> (\v1, v2 => Fin $ DPair.fst $ decidableFilter (v1, v2) edges) +> (\v1, v2 => Fin $ fst $ decEqFilter (v1, v2) edges) From ed699b2b2f7e8576d50858d41af117cef0f1cc9a Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 12 Nov 2019 09:38:13 +0100 Subject: [PATCH 10/15] prove that the first element is kept by filtering --- src/Free/Path.lidr | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr index c7defb6..ae66243 100644 --- a/src/Free/Path.lidr +++ b/src/Free/Path.lidr @@ -54,10 +54,14 @@ along with this program. If not, see . > Empty : EdgeListPath edges i i > Cons : Elem (i, j) edges -> EdgeListPath edges j k -> EdgeListPath edges i k > -> -> filterElemWhichIsHere : Eq t => (x : t) -> (l : Vect _ t) -> (k : Nat ** DPair.fst $ filter ((==) x) (x :: l) = S k) -> filterElemWhichIsHere x [] = (0 ** ?asdf) -> filterElemWhichIsHere x xs = ?qwer +> filterElemWhichIsHere : DecEq t => (x : t) -> (l : Vect _ t) -> (k : Nat ** fst $ decEqFilter x (x :: l) = S k) +> filterElemWhichIsHere x [] with (decEq x x) +> filterElemWhichIsHere x [] | Yes Refl = (0 ** Refl) +> filterElemWhichIsHere x [] | No contra = void $ contra Refl +> filterElemWhichIsHere x xs with (decEq x x) +> filterElemWhichIsHere x xs | Yes Refl with (decEqFilter x xs) +> filterElemWhichIsHere x xs | Yes Refl | (i ** vs) = (i ** Refl) +> filterElemWhichIsHere x xs | No contra = void $ contra Refl > > -- countOccurence : Eq vertices => {v1, v2 : vertices} -> Elem (v1, v2) edges -> Fin $ fst $ filter ((==) (v1, v2)) edges > -- countOccurence {edges = (v1 , v2 ) :: l} Here = rewrite DPair.snd $ filterElemWhichIsHere l (v1, v2) in 0 From d8c5ecf2004f08041b05c66e1f1b06a29d28a820 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 12 Nov 2019 16:38:10 +0100 Subject: [PATCH 11/15] complete proofs for edgeListPath --- src/Free/Path.lidr | 44 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 34 insertions(+), 10 deletions(-) diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr index ae66243..c8395e0 100644 --- a/src/Free/Path.lidr +++ b/src/Free/Path.lidr @@ -63,14 +63,38 @@ along with this program. If not, see . > filterElemWhichIsHere x xs | Yes Refl | (i ** vs) = (i ** Refl) > filterElemWhichIsHere x xs | No contra = void $ contra Refl > -> -- countOccurence : Eq vertices => {v1, v2 : vertices} -> Elem (v1, v2) edges -> Fin $ fst $ filter ((==) (v1, v2)) edges -> -- countOccurence {edges = (v1 , v2 ) :: l} Here = rewrite DPair.snd $ filterElemWhichIsHere l (v1, v2) in 0 -> -- countOccurence {v1} {v2} {edges = (v1', v2') :: l} (There a) = let rec = countOccurence a in if (v1', v2') == (v1,v2) then weaken rec else ?qwer +> countOccurrence : DecEq vertices +> => {i, j : vertices} +> -> (edges : Vect n (vertices, vertices)) +> -> Elem (i, j) edges +> -> Fin $ fst $ decEqFilter (i, j) edges +> countOccurrence {i} {j} ((i, j) :: xs) Here with (decEq (i,j) (i,j)) +> countOccurrence {i} {j} ((i, j) :: xs) Here | Yes Refl with (decEqFilter (i, j) xs) +> countOccurrence {i} {j} ((i, j) :: xs) Here | Yes Refl | (k ** vs) = 0 +> countOccurrence {i} {j} ((i, j) :: xs) Here | No contra = void $ contra Refl +> countOccurrence {i} {j} ((k, l) :: xs) (There e) with (decEq (i, j) (k, l)) +> countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl with (decEq (i, j) (i, j)) +> countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | Yes Refl with (decEqFilter (i, j) xs) proof prf +> countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | Yes Refl | (k ** vs) +> = FS $ rewrite cong {f=DPair.fst} prf in countOccurrence {i} {j} xs e +> countOccurrence {i} {j} ((i, j) :: xs) (There e) | Yes Refl | No contra = void $ contra Refl +> countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra with (decEqFilter (i, j) xs) proof prf +> countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) with (decEq k i) +> countOccurrence {i} {j} ((i, l) :: xs) (There e) | No contra | (m ** vs) | Yes Refl with (decEq l j) +> countOccurrence {i} {j} ((i, j) :: xs) (There e) | No contra | (m ** vs) | Yes Refl | Yes Refl +> = void $ contra Refl +> countOccurrence {i} {j} ((i, l) :: xs) (There e) | No contra | (m ** vs) | Yes Refl | No contra' +> = countOccurrence {i} {j} xs e +> countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) | No contra' with (decEq l j) +> countOccurrence {i} {j} ((k, j) :: xs) (There e) | No contra | (m ** vs) | No contra' | Yes Refl +> = countOccurrence {i} {j} xs e +> countOccurrence {i} {j} ((k, l) :: xs) (There e) | No contra | (m ** vs) | No contra' | No contra'' +> = countOccurrence {i} {j} xs e > -> -- edgeListPath : Eq vertices -> -- => {edges : Vect n (vertices, vertices)} -> -- -> {i, j : vertices} -> -- -> EdgeListPath edges i j -> -- -> Path (edgeList edges) i j -> -- edgeListPath Empty = Nil -> -- edgeListPath (Cons elem elp) = (countOccurence {edges} elem) :: (edgeListPath elp) +> edgeListPath : DecEq vertices +> => {edges : Vect n (vertices, vertices)} +> -> {i, j : vertices} +> -> EdgeListPath edges i j +> -> Path (edgeList edges) i j +> edgeListPath Empty = Nil +> edgeListPath (Cons elem elp) = (countOccurrence edges elem) :: (edgeListPath elp) From 22d7154a1859ba15764bc460a9382e2d9123286b Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 12 Nov 2019 16:50:57 +0100 Subject: [PATCH 12/15] add DecEq instance for Pushout graph --- src/CoLimits/Pushout.lidr | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/CoLimits/Pushout.lidr b/src/CoLimits/Pushout.lidr index f134b23..d7e8ca8 100644 --- a/src/CoLimits/Pushout.lidr +++ b/src/CoLimits/Pushout.lidr @@ -33,11 +33,25 @@ along with this program. If not, see . > > data PushoutIndexObject = X | Y | Z > -> Eq PushoutIndexObject where -> X == X = True -> Y == Y = True -> Z == Z = True -> _ == _ = False +> XnotY : X = Y -> Void +> XnotY Refl impossible +> +> XnotZ : X = Z -> Void +> XnotZ Refl impossible +> +> YnotZ : Y = Z -> Void +> YnotZ Refl impossible +> +> DecEq PushoutIndexObject where +> decEq X X = Yes Refl +> decEq X Y = No XnotY +> decEq X Z = No XnotZ +> decEq Y X = No (negEqSym XnotY) +> decEq Y Y = Yes Refl +> decEq Y Z = No YnotZ +> decEq Z X = No (negEqSym XnotZ) +> decEq Z Y = No (negEqSym YnotZ) +> decEq Z Z = Yes Refl > > PushoutIndexGraph : Graph > PushoutIndexGraph = edgeList [(Z, X), (Z, Y)] From 2487fca6e8807f380752b0a2a4561652c98f0922 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 12 Nov 2019 16:51:24 +0100 Subject: [PATCH 13/15] remove finite version of Graph --- 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 ---------------------------- 5 files changed, 223 deletions(-) delete mode 100644 src/Free/Finite/FinGraph.lidr delete mode 100644 src/Free/Finite/FinPath.lidr delete mode 100644 src/Free/Finite/FinPathCategory.lidr delete mode 100644 src/Free/Finite/FreeFinFunctor.lidr diff --git a/idris-ct.ipkg b/idris-ct.ipkg index 0e308fb..b1e9a07 100644 --- a/idris-ct.ipkg +++ b/idris-ct.ipkg @@ -45,10 +45,6 @@ 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 deleted file mode 100644 index 9baae2f..0000000 --- a/src/Free/Finite/FinGraph.lidr +++ /dev/null @@ -1,46 +0,0 @@ -\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 deleted file mode 100644 index 958a041..0000000 --- a/src/Free/Finite/FinPath.lidr +++ /dev/null @@ -1,60 +0,0 @@ -\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 deleted file mode 100644 index 4386c5d..0000000 --- a/src/Free/Finite/FinPathCategory.lidr +++ /dev/null @@ -1,40 +0,0 @@ -\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.Finite.FinGraph -> import Free.Finite.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 deleted file mode 100644 index 0266192..0000000 --- a/src/Free/Finite/FreeFinFunctor.lidr +++ /dev/null @@ -1,73 +0,0 @@ -\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) From b1642e9b408a5ec9079b5835204a648393026d37 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Thu, 21 Nov 2019 09:33:15 +0100 Subject: [PATCH 14/15] correct indentation --- src/Monad/KleisliCategory.lidr | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/Monad/KleisliCategory.lidr b/src/Monad/KleisliCategory.lidr index 5997ede..7b408c3 100644 --- a/src/Monad/KleisliCategory.lidr +++ b/src/Monad/KleisliCategory.lidr @@ -40,13 +40,17 @@ along with this program. If not, see . > (component (multiplication m) c)) > (\a, b, f => trans (cong {f = \x => compose cat _ _ _ x (component (multiplication m) b)} > (commutativity (unit m) a (mapObj (functor m) b) f)) -> (trans (sym $ associativity cat _ _ _ _ -> f -> (component (unit m) (mapObj (functor m) b)) -> (component (multiplication m) b)) -> (trans (cong {f = \x => compose cat _ _ _ f (component x b)} -> (leftUnit m)) -> (rightIdentity cat a (mapObj (functor m) b) f)))) +> (trans (sym $ associativity cat +> a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) b)) +> (mapObj (functor m) b) +> f +> (component (unit m) (mapObj (functor m) b)) +> (component (multiplication m) b)) +> (trans (cong {f = \x => compose cat a (mapObj (functor m) b) (mapObj (functor m) b) f (component x b)} +> (leftUnit m)) +> (rightIdentity cat a (mapObj (functor m) b) f)))) > (\a, b, f => trans (sym $ associativity cat _ _ _ _ > f > (mapMor (functor m) _ _ (component (unit m) b)) From 1efb34427f9d664288055234de84b6d548292806 Mon Sep 17 00:00:00 2001 From: Marco Perone Date: Tue, 26 Nov 2019 11:32:05 +0100 Subject: [PATCH 15/15] split Kleisli category for faster compile time --- src/Monad/KleisliCategory.lidr | 227 +----------------- src/Monad/KleisliCategoryHelpers.lidr | 329 ++++++++++++++++++++++++++ 2 files changed, 333 insertions(+), 223 deletions(-) create mode 100644 src/Monad/KleisliCategoryHelpers.lidr diff --git a/src/Monad/KleisliCategory.lidr b/src/Monad/KleisliCategory.lidr index 7b408c3..fcf850c 100644 --- a/src/Monad/KleisliCategory.lidr +++ b/src/Monad/KleisliCategory.lidr @@ -24,8 +24,7 @@ along with this program. If not, see . > import Basic.Category > import Basic.Functor > import Basic.NaturalTransformation -> import Cats.CatsAsCategory -> import Cats.FunctorsAsCategory +> import Monad.KleisliCategoryHelpers > import Monad.Monad > > %access public export @@ -38,224 +37,6 @@ along with this program. If not, see . > (component (unit m)) > (\a, b, c, f, g => compose cat _ _ _ (compose cat _ _ _ f (mapMor (functor m) _ _ g)) > (component (multiplication m) c)) -> (\a, b, f => trans (cong {f = \x => compose cat _ _ _ x (component (multiplication m) b)} -> (commutativity (unit m) a (mapObj (functor m) b) f)) -> (trans (sym $ associativity cat -> a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) b)) -> (mapObj (functor m) b) -> f -> (component (unit m) (mapObj (functor m) b)) -> (component (multiplication m) b)) -> (trans (cong {f = \x => compose cat a (mapObj (functor m) b) (mapObj (functor m) b) f (component x b)} -> (leftUnit m)) -> (rightIdentity cat a (mapObj (functor m) b) f)))) -> (\a, b, f => trans (sym $ associativity cat _ _ _ _ -> f -> (mapMor (functor m) _ _ (component (unit m) b)) -> (component (multiplication m) b)) -> (trans (cong {f = \x => compose cat _ _ _ f (component x b)} -> (rightUnit m)) -> (rightIdentity cat _ _ f))) -> (\a, b, c, d, f, g, h => -> trans (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) d)) -> f -> x) -> (component (multiplication m) d)} -> (preserveCompose (functor m) b -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (compose cat b -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> g -> (mapMor (functor m) c (mapObj (functor m) d) h)) -> (component (multiplication m) d))) -> (trans (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> x -> (component (multiplication m) d)} -> (associativity cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> f -> (mapMor (functor m) b -> (mapObj (functor m) (mapObj (functor m) d)) -> (compose cat b -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> g -> (mapMor (functor m) c -> (mapObj (functor m) d) -> h))) -> (mapMor (functor m) (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) d)))) -> (trans (sym $ associativity cat a -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> f -> (mapMor (functor m) b -> (mapObj (functor m) (mapObj (functor m) d)) -> (compose cat b -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> g -> (mapMor (functor m) c -> (mapObj (functor m) d) -> h)))) -> (mapMor (functor m) (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) d)) -> (component (multiplication m) d)) -> (trans (cong {f = compose cat a -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> f -> (mapMor (functor m) b -> (mapObj (functor m) (mapObj (functor m) d)) -> (compose cat b -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> g -> (mapMor (functor m) c -> (mapObj (functor m) d) -> h))))} -> (cong {f = \x => component x d} (associativity m))) -> (trans (cong $ leftIdentity cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) d) -> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) (mapObj (functor m) d)) -> (component (multiplication m) d))) -> (trans (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> f -> x) -> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) (mapObj (functor m) d)) -> (component (multiplication m) d))} -> (preserveCompose (functor m) b -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> g -> (mapMor (functor m) c (mapObj (functor m) d) h))) -> (trans (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) d) -> x -> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) (mapObj (functor m) d)) -> (component (multiplication m) d))} -> (associativity cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g) -> (mapMor (functor m) (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapMor (functor m) c (mapObj (functor m) d) h)))) -> (trans (sym $ associativity cat a -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g)) -> (mapMor (functor m) (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapMor (functor m) c (mapObj (functor m) d) h)) -> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (component (multiplication m) (mapObj (functor m) d)) -> (component (multiplication m) d))) -> (trans (cong {f = compose cat a -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g))} -> (associativity cat (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (mapMor (functor m) (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapMor (functor m) c (mapObj (functor m) d) h)) -> (component (multiplication m) (mapObj (functor m) d)) -> (component (multiplication m) d))) -> (trans (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g)) -> (compose cat (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> x -> (component (multiplication m) d))} -> (sym $ commutativity (multiplication m) c (mapObj (functor m) d) h)) -> (trans (associativity cat a -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g)) -> (compose cat (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> (component (multiplication m) c) -> (mapMor (functor m) c (mapObj (functor m) d) h)) -> (component (multiplication m) d)) -> (cong {f = \x => compose cat a -> (mapObj (functor m) (mapObj (functor m) d)) -> (mapObj (functor m) d) -> x -> (component (multiplication m) d)} -> (associativity cat a -> (mapObj (functor m) (mapObj (functor m) c)) -> (mapObj (functor m) c) -> (mapObj (functor m) (mapObj (functor m) d)) -> (compose cat a -> (mapObj (functor m) b) -> (mapObj (functor m) (mapObj (functor m) c)) -> f -> (mapMor (functor m) b (mapObj (functor m) c) g)) -> (component (multiplication m) c) -> (mapMor (functor m) c (mapObj (functor m) d) h)))))))))))))) +> (kleisliCategoryLeftIdentity {cat} m) +> (kleisliCategoryRightIdentity {cat} m) +> (kleisliCategoryAssociativity {cat} m) diff --git a/src/Monad/KleisliCategoryHelpers.lidr b/src/Monad/KleisliCategoryHelpers.lidr new file mode 100644 index 0000000..751a109 --- /dev/null +++ b/src/Monad/KleisliCategoryHelpers.lidr @@ -0,0 +1,329 @@ +\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 Monad.KleisliCategoryHelpers +> +> import Basic.Category +> import Basic.Functor +> import Basic.NaturalTransformation +> import Monad.Monad +> +> %access public export +> %default total +> +> kleisliCategoryLeftIdentity : +> {cat : Category} +> -> (m : Monad cat) +> -> (a, b : obj cat) +> -> (f : mor cat a (mapObj (functor m) b)) +> -> compose cat a +> (mapObj (functor m) (mapObj (functor m) b)) +> (mapObj (functor m) b) +> (compose cat a +> (mapObj (functor m) a) +> (mapObj (functor m) (mapObj (functor m) b)) +> (component (unit m) a) +> (mapMor (functor m) a (mapObj (functor m) b) f)) +> (component (multiplication m) b) +> = f +> kleisliCategoryLeftIdentity {cat} m a b f = +> trans (cong {f = \x => compose cat _ _ _ x (component (multiplication m) b)} +> (commutativity (unit m) a (mapObj (functor m) b) f)) +> (trans (sym $ associativity cat +> a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) b)) +> (mapObj (functor m) b) +> f +> (component (unit m) (mapObj (functor m) b)) +> (component (multiplication m) b)) +> (trans (cong {f = \x => compose cat a (mapObj (functor m) b) (mapObj (functor m) b) f (component x b)} +> (leftUnit m)) +> (rightIdentity cat a (mapObj (functor m) b) f))) +> +> kleisliCategoryRightIdentity : +> {cat : Category} +> -> (m : Monad cat) +> -> (a, b : obj cat) +> -> (f : mor cat a (mapObj (functor m) b)) +> -> compose cat a +> (mapObj (functor m) (mapObj (functor m) b)) +> (mapObj (functor m) b) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) b)) +> f +> (mapMor (functor m) b (mapObj (functor m) b) (component (unit m) b))) +> (component (multiplication m) b) +> = f +> kleisliCategoryRightIdentity {cat} m a b f = +> trans (sym $ associativity cat _ _ _ _ +> f +> (mapMor (functor m) _ _ (component (unit m) b)) +> (component (multiplication m) b)) +> (trans (cong {f = \x => compose cat _ _ _ f (component x b)} +> (rightUnit m)) +> (rightIdentity cat _ _ f)) +> +> kleisliCategoryAssociativity : +> {cat : Category} +> -> (m : Monad cat) +> -> (a, b, c, d : obj cat) +> -> (f : mor cat a (mapObj (functor m) b)) +> -> (g : mor cat b (mapObj (functor m) c)) +> -> (h : mor cat c (mapObj (functor m) d)) +> -> compose cat a +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) d)) +> f +> (mapMor (functor m) b +> (mapObj (functor m) d) +> (compose cat b +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (component (multiplication m) d)))) +> (component (multiplication m) d) +> = compose cat a +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (compose cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) c) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g)) +> (component (multiplication m) c)) +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (component (multiplication m) d) +> kleisliCategoryAssociativity {cat} m a b c d f g h = +> trans (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) d)) +> f +> x) +> (component (multiplication m) d)} +> (preserveCompose (functor m) b +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (component (multiplication m) d))) +> (trans (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> x +> (component (multiplication m) d)} +> (associativity cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> f +> (mapMor (functor m) b +> (mapObj (functor m) (mapObj (functor m) d)) +> (compose cat b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c +> (mapObj (functor m) d) +> h))) +> (mapMor (functor m) (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) d)))) +> (trans (sym $ associativity cat a +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> f +> (mapMor (functor m) b +> (mapObj (functor m) (mapObj (functor m) d)) +> (compose cat b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c +> (mapObj (functor m) d) +> h)))) +> (mapMor (functor m) (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) d)) +> (component (multiplication m) d)) +> (trans (cong {f = compose cat a +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> f +> (mapMor (functor m) b +> (mapObj (functor m) (mapObj (functor m) d)) +> (compose cat b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c +> (mapObj (functor m) d) +> h))))} +> (cong {f = \x => component x d} (associativity m))) +> (trans (cong $ leftIdentity cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) d) +> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) (mapObj (functor m) d)) +> (component (multiplication m) d))) +> (trans (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> f +> x) +> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) (mapObj (functor m) d)) +> (component (multiplication m) d))} +> (preserveCompose (functor m) b +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> g +> (mapMor (functor m) c (mapObj (functor m) d) h))) +> (trans (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) d) +> x +> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) (mapObj (functor m) d)) +> (component (multiplication m) d))} +> (associativity cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g) +> (mapMor (functor m) (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapMor (functor m) c (mapObj (functor m) d) h)))) +> (trans (sym $ associativity cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g)) +> (mapMor (functor m) (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (compose cat (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (component (multiplication m) (mapObj (functor m) d)) +> (component (multiplication m) d))) +> (trans (cong {f = compose cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g))} +> (associativity cat (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) (mapObj (functor m) (mapObj (functor m) d))) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (mapMor (functor m) (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (component (multiplication m) (mapObj (functor m) d)) +> (component (multiplication m) d))) +> (trans (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g)) +> (compose cat (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> x +> (component (multiplication m) d))} +> (sym $ commutativity (multiplication m) c (mapObj (functor m) d) h)) +> (trans (associativity cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g)) +> (compose cat (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (component (multiplication m) c) +> (mapMor (functor m) c (mapObj (functor m) d) h)) +> (component (multiplication m) d)) +> (cong {f = \x => compose cat a +> (mapObj (functor m) (mapObj (functor m) d)) +> (mapObj (functor m) d) +> x +> (component (multiplication m) d)} +> (associativity cat a +> (mapObj (functor m) (mapObj (functor m) c)) +> (mapObj (functor m) c) +> (mapObj (functor m) (mapObj (functor m) d)) +> (compose cat a +> (mapObj (functor m) b) +> (mapObj (functor m) (mapObj (functor m) c)) +> f +> (mapMor (functor m) b (mapObj (functor m) c) g)) +> (component (multiplication m) c) +> (mapMor (functor m) c (mapObj (functor m) d) h)))))))))))))