diff --git a/Kleisli.agda b/Kleisli.agda new file mode 100644 index 0000000..b1eb149 --- /dev/null +++ b/Kleisli.agda @@ -0,0 +1,3 @@ + +-- Here we definition the notion of kleisli-triple and prove that it is equivalent to a monad +record Kleisli \ No newline at end of file diff --git a/Kleisli.agda-lib b/Kleisli.agda-lib new file mode 100644 index 0000000..cc04801 --- /dev/null +++ b/Kleisli.agda-lib @@ -0,0 +1,3 @@ +name: kleisli +include: . +depend: agda-categories standard-library