From cbebb74423b875f7d571584079cd1e4d1c31965e Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 10:57:36 -0500
Subject: [PATCH] Add Data.Tensor

I should have done this earlier, but I forgot to.
---
 Data/Tensor.idr  | 62 ++++++++++++++++++++++++++++++++++++++++++++++++
 profunctors.ipkg |  5 +++-
 2 files changed, 66 insertions(+), 1 deletion(-)
 create mode 100644 Data/Tensor.idr

diff --git a/Data/Tensor.idr b/Data/Tensor.idr
new file mode 100644
index 0000000..35d25c5
--- /dev/null
+++ b/Data/Tensor.idr
@@ -0,0 +1,62 @@
+module Data.Tensor
+
+%default total
+
+
+public export
+record Isomorphism a b where
+  constructor MkIso
+  fwd : a -> b
+  bwd : b -> a
+
+
+public export
+interface Bifunctor ten => Associative ten where
+  assoc : Isomorphism (a `ten` (b `ten` c)) ((a `ten` b) `ten` c)
+
+public export
+interface Bifunctor ten => Symmetric ten where
+  swap : a `ten` b -> b `ten` a
+
+
+public export
+interface Associative ten => Tensor ten i | ten where
+  unitl : Isomorphism (i `ten` a) a
+  unitr : Isomorphism (a `ten` i) a
+
+
+export
+Associative Pair where
+  assoc = MkIso (\(x,(y,z)) => ((x,y),z)) (\((x,y),z) => (x,(y,z)))
+
+export
+Symmetric Pair where
+  swap = Builtin.swap
+
+export
+Tensor Pair () where
+  unitl = MkIso snd ((),)
+  unitr = MkIso fst (,())
+
+
+export
+Associative Either where
+  assoc = MkIso f b
+    where
+      f : forall a,b,c. Either a (Either b c) -> Either (Either a b) c
+      f (Left x) = Left (Left x)
+      f (Right (Left x)) = Left (Right x)
+      f (Right (Right x)) = Right x
+
+      b : forall a,b,c. Either (Either a b) c -> Either a (Either b c)
+      b (Left (Left x)) = Left x
+      b (Left (Right x)) = Right (Left x)
+      b (Right x) = Right (Right x)
+
+export
+Symmetric Either where
+  swap = either Right Left
+
+Tensor Either Void where
+  unitl = MkIso (either absurd id) Right
+  unitr = MkIso (either id absurd) Left
diff --git a/profunctors.ipkg b/profunctors.ipkg
index 8bea9f4..342f1da 100644
--- a/profunctors.ipkg
+++ b/profunctors.ipkg
@@ -6,4 +6,7 @@ license = "MIT"
 
 readme = "README.md"
 
-modules = Data.Profunctor.Types
+modules = Data.Tensor,
+          Data.Profunctor.Types,
+          Data.Profunctor.Functor,
+          Data.Profunctor.Strong