1 files changed, 115 insertions, 0 deletions
diff --git a/src/Data/Setoid/Pair.idr b/src/Data/Setoid/Pair.idr
new file mode 100644
index 0000000..2cb9357
--- /dev/null
+++ b/src/Data/Setoid/Pair.idr
@@ -0,0 +1,115 @@
+||| Product of setoids
+module Data.Setoid.Pair
+
+import Data.Setoid.Definition
+import Data.Setoid.Either
+
+%default total
+
+||| Binary relation conjunction
+public export
+record And {A,B : Type} (p : Rel A) (q : Rel B) (xy1, xy2 : (A, B)) where
+  constructor MkAnd
+  fst : p (fst xy1) (fst xy2)
+  snd : q (snd xy1) (snd xy2)
+
+||| Product of setoids
+public export
+Pair : (a,b : Setoid) -> Setoid
+Pair a b = MkSetoid
+  { U = (U a, U b)
+  , equivalence = MkEquivalence
+    { relation = a.equivalence.relation `And` b.equivalence.relation
+    , reflexive = \xy => MkAnd
+        (a.equivalence.reflexive $ fst xy)
+        (b.equivalence.reflexive $ snd xy)
+    , symmetric  = \xy1,xy2,prf => MkAnd
+        (a.equivalence.symmetric (fst xy1) (fst xy2) prf.fst)
+        (b.equivalence.symmetric (snd xy1) (snd xy2) prf.snd)
+    , transitive = \xy1,xy2,xy3,prf1,prf2 => MkAnd
+        (a.equivalence.transitive (fst xy1) (fst xy2) (fst xy3) prf1.fst prf2.fst)
+        (b.equivalence.transitive (snd xy1) (snd xy2) (snd xy3) prf1.snd prf2.snd)
+    }
+  }
+
+||| Left projection setoid homomorphism
+public export
+(.fst) : {0 a,b : Setoid} -> Pair a b ~> a
+(.fst) = MkSetoidHomomorphism
+  { H = Builtin.fst
+  , homomorphic = \xy1,xy2,prf => prf.fst
+  }
+
+||| Right projection setoid homomorphism
+public export
+(.snd) : {0 a,b : Setoid} -> Pair a b ~> b
+(.snd) = MkSetoidHomomorphism
+  { H = Builtin.snd
+  , homomorphic = \xy1,xy2,prf => prf.snd
+  }
+
+||| Setoid homomorphism constructor
+public export
+tuple : {0 a,b,c : Setoid} -> c ~> a -> c ~> b -> c ~> Pair a b
+tuple f g = MkSetoidHomomorphism
+  { H = \z => (f.H z, g.H z)
+  , homomorphic = \z1,z2,prf => MkAnd
+      (f.homomorphic z1 z2 prf)
+      (g.homomorphic z1 z2 prf)
+  }
+
+||| Unique value of type unit
+public export
+unitVal : (x,y : Unit) -> x = y
+unitVal () () = Refl
+
+||| The unique setoid map into the terminal type
+public export
+unit : {a : Setoid} -> a ~> cast Unit
+unit = MkSetoidHomomorphism
+  { H = const ()
+  , homomorphic = \_,_,_ => unitVal () ()
+  }
+
+||| The constant function as a setoid morphism
+public export
+const : {a,b : Setoid} -> (x : U b) -> a ~> b
+const x = mate (Prelude.const x) . unit
+
+||| Setoid homomorphism constructor
+public export
+bimap : {a,b,c,d : Setoid} -> c ~> a -> d ~> b -> Pair c d ~> Pair a b
+bimap f g = tuple (f . (.fst)) (g . (.snd))
+
+-- Distribution of products over sums, degenerate case:
+
+||| Function underlying the bijection 2 x s <~> s + s
+public export
+distributeFunction : {s : Setoid} -> (Bool, U s) -> (U s `Either` U s)
+distributeFunction (False, x) = Left  x
+distributeFunction (True , x) = Right x
+
+||| States: the function underlying the bijection 2 x s <~> s + s is a setoid homomorphism
+public export
+distributeHomomorphism : {s : Setoid} ->
+  SetoidHomomorphism ((cast Bool) `Pair` s) (s `Either` s)
+    (distributeFunction {s})
+distributeHomomorphism (b1,x1) (b2,x2) prf =
+  case prf.fst of
+    Refl => case b2 of
+      False => Left  prf.snd
+      True  => Right prf.snd
+
+||| Setoid homomorphism involved in the bijection 2 x s <~> s + s
+public export
+distribute : {s : Setoid} -> ((cast Bool) `Pair` s) ~> (s `Either` s)
+distribute = MkSetoidHomomorphism
+  { H = distributeFunction
+  , homomorphic = distributeHomomorphism
+  }
+
+public export
+pairIso : {a,b,c,d : Setoid} -> (a <~> c) -> (b <~> d) -> (Pair a b <~> Pair c d)
+pairIso ac bd = MkIsomorphism (bimap ac.Fwd bd.Fwd) (bimap ac.Bwd bd.Bwd)
+                  (IsIsomorphism (\(x,y) => MkAnd (ac.Iso.BwdFwdId x) (bd.Iso.BwdFwdId y))
+                                 (\(x,y) => MkAnd (ac.Iso.FwdBwdId x) (bd.Iso.FwdBwdId y)))