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/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)]
diff --git a/src/CoLimits/Pushout.lidr b/src/CoLimits/Pushout.lidr
index 4d59245..d7e8ca8 100644
--- a/src/CoLimits/Pushout.lidr
+++ b/src/CoLimits/Pushout.lidr
@@ -33,10 +33,28 @@ along with this program. If not, see .
>
> data PushoutIndexObject = X | Y | Z
>
+> 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 = MkGraph
-> PushoutIndexObject
-> [(Z, X), (Z, Y)]
+> PushoutIndexGraph = edgeList [(Z, X), (Z, Y)]
>
> PushoutIndexCategory : Category
> PushoutIndexCategory = pathCategory PushoutIndexGraph
diff --git a/src/Free/FreeFunctor.lidr b/src/Free/FreeFunctor.lidr
index b695de4..c29a830 100644
--- a/src/Free/FreeFunctor.lidr
+++ b/src/Free/FreeFunctor.lidr
@@ -23,7 +23,6 @@ along with this program. If not, see .
>
> import Basic.Category
> import Basic.Functor
-> import Data.Vect
> import Free.Graph
> import Free.Path
> import Free.PathCategory
@@ -34,7 +33,7 @@ along with this program. If not, see .
> 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)
diff --git a/src/Free/Graph.lidr b/src/Free/Graph.lidr
index 5bc70b2..2a6b244 100644
--- a/src/Free/Graph.lidr
+++ b/src/Free/Graph.lidr
@@ -29,18 +29,17 @@ along with this program. If not, see .
> record Graph where
> constructor MkGraph
> vertices : Type
-> edges : Vect n (vertices, vertices)
+> edges : vertices -> vertices -> Type
>
-> Edge : (g : Graph) -> (i, j : vertices g) -> Type
-> Edge g i j = Elem (i, j) (edges g)
+> 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
>
-> 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)]
+> edgeList : DecEq vertices
+> => (edges : Vect n (vertices, vertices))
+> -> Graph
+> edgeList edges = MkGraph
+> vertices
+> (\v1, v2 => Fin $ fst $ decEqFilter (v1, v2) edges)
diff --git a/src/Free/Path.lidr b/src/Free/Path.lidr
index 763c666..c8395e0 100644
--- a/src/Free/Path.lidr
+++ b/src/Free/Path.lidr
@@ -21,7 +21,7 @@ along with this program. If not, see .
> module Free.Path
>
-> import Data.List
+> import Data.Vect
> import Free.Graph
>
> %access public export
@@ -29,18 +29,9 @@ along with this program. If not, see .
>
> 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)
+> (::) : 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
@@ -58,3 +49,52 @@ oneToThree' = Here :: There Here :: Nil
> -> 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 : 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
+>
+> 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 : 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)
diff --git a/src/Monad/KleisliCategory.lidr b/src/Monad/KleisliCategory.lidr
index 5997ede..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,220 +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 _ _ _ _
-> 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))))
-> (\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)))))))))))))