refactor: reorder definitions.

1 files changed, 61 insertions, 41 deletions

diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 041d650..0e63acc 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -65,6 +65,22 @@ parameters {0 x, y : RawSetoidAlgebra sig}
   tmRelsImpliesCoprodRels []          = []
   tmRelsImpliesCoprodRels (eq :: eqs) = tmRelImpliesCoprodRel eq :: tmRelsImpliesCoprodRels eqs
 
+namespace Rel
+  public export
+  CoproductSet : (0 sig : Signature) -> (x, y : Algebra sig) -> IndexedSetoid sig.T
+  CoproductSet sig x y = MkIndexedSetoid
+    { U           = CoproductSet sig x.raw.U y.raw.U
+    , equivalence = MkIndexedEquivalence
+      { relation   = (~=~) x.rawSetoid y.rawSetoid
+      , reflexive  = \_ =>
+        coprodRelRefl
+          x.algebra.equivalence.reflexive
+          y.algebra.equivalence.reflexive
+      , symmetric  = \_, _, _ => Sym
+      , transitive = \_, _, _, _ => Trans {x = x.rawSetoid, y = y.rawSetoid}
+      }
+    }
+
 public export
 Coproduct : (x, y : RawAlgebra sig) -> RawAlgebra sig
 Coproduct x y = MkRawAlgebra
@@ -73,39 +89,51 @@ Coproduct x y = MkRawAlgebra
   }
 
 public export
-CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y
-  -> IsAlgebra sig (Coproduct x y)
-CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
-  { equivalence = MkIndexedEquivalence
-    { relation   =
-        (~=~)
-          (MkRawSetoidAlgebra x xIsAlgebra.equivalence.relation)
-          (MkRawSetoidAlgebra y yIsAlgebra.equivalence.relation)
-    , reflexive  = \_ =>
-      coprodRelRefl
-        xIsAlgebra.equivalence.reflexive
-        yIsAlgebra.equivalence.reflexive
-    , symmetric  = \_, _, _ => Sym
-    , transitive = \_, _, _, _ => Trans
-    }
-  , semCong = Call
+CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
+CoproductAlgebra x y = MkAlgebra
+  { U   = CoproductSet sig x y
+  , sem = \op => MkSetoidHomomorphism (Call op) (\_, _ => Call op)
+
   }
 
 public export
-CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MakeAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
+fromTerm : (0 x, y : Algebra sig)
+  -> Term sig (bundle $ \i => Either (index x.setoid i) (index y.setoid i))
+  ~> CoproductSet sig x y
+fromTerm x y = MkIndexedSetoidHomomorphism (\_ => id) (\_, _, _ => tmRelImpliesCoprodRel)
+
+public export
+fromFree : (x, y : Algebra sig)
+  -> FreeAlgebra (bundle (\t => Either (index x.setoid t) (index y.setoid t)))
+  ~> CoproductAlgebra x y
+fromFree x y = MkHomomorphism
+  { func    = fromTerm x y
+  , semHomo = \op, tms =>
+    Call op $
+    reflect (index (Product (CoproductAlgebra x y).setoid) _) $
+    sym $
+    mapId tms
+  }
 
 public export
-injectLHomo : x ~> CoproductAlgebra x y
+injectLHomo : {x, y : Algebra sig} -> x ~> CoproductAlgebra x y
 injectLHomo = MkHomomorphism
-  { func    = MkIndexedSetoidHomomorphism (\_ => Done . Left) (\_, _, _ => DoneL)
+  { func    = bundle (\t =>
+    index
+      {x = bundle (\t => Either (index x.setoid t) (index y.setoid t))}
+      (fromTerm x y . injectFunc) t .
+    Left)
   , semHomo = InjectL
   }
 
 public export
-injectRHomo : y ~> CoproductAlgebra x y
+injectRHomo : {x, y : Algebra sig} -> y ~> CoproductAlgebra x y
 injectRHomo = MkHomomorphism
-  { func    = MkIndexedSetoidHomomorphism (\_ => Done . Right) (\_, _, _ => DoneR)
+  { func    = bundle (\t =>
+    index
+      {x = bundle (\t => Either (index x.setoid t) (index y.setoid t))}
+      (fromTerm x y . injectFunc) t .
+    Right)
   , semHomo = InjectR
   }
 
@@ -154,13 +182,18 @@ coproductsCong f g []          = []
 coproductsCong f g (eq :: eqs) = coproductCong f g eq :: coproductsCong f g eqs
 
 public export
+coproductFunc : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+  -> CoproductSet sig x y ~> z.setoid
+coproductFunc f g = MkIndexedSetoidHomomorphism
+  { H           = coproduct {z = z.raw} f.func.H g.func.H
+  , homomorphic = \_, _, _ => coproductCong f g
+  }
+
+public export
 coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
   -> CoproductAlgebra x y ~> z
 coproductHomo f g = MkHomomorphism
-  { func = MkIndexedSetoidHomomorphism
-    { H           = coproduct {z = z.raw} f.func.H g.func.H
-    , homomorphic = \_, _, _ => coproductCong f g
-    }
+  { func = coproductFunc f g
   , semHomo = \op, tms =>
     reflect (index z.setoid _) $
     cong (z.raw.sem op) $
@@ -168,19 +201,6 @@ coproductHomo f g = MkHomomorphism
   }
 
 public export
-termToCoproduct : (x, y : Algebra sig)
-  -> FreeAlgebra (bundle (\t => Either (index x.setoid t) (index y.setoid t))) ~>
-     CoproductAlgebra x y
-termToCoproduct x y = MkHomomorphism
-  { func    = MkIndexedSetoidHomomorphism (\_ => id) (\t, _, _ => tmRelImpliesCoprodRel)
-  , semHomo = \op, tms =>
-    Call op $
-    reflect (index (Product (CoproductAlgebra x y).setoid) _) $
-    sym $
-    mapId tms
-  }
-
-public export
 coproductUnique' : {x, y, z : Algebra sig}
   -> (f : CoproductAlgebra x y ~> z)
   -> (g : CoproductAlgebra x y ~> z)
@@ -192,8 +212,8 @@ coproductUnique' : {x, y, z : Algebra sig}
   -> z.relation t (f.func.H t tm) (g.func.H t tm)
 coproductUnique' f g congL congR tm = bindUnique'
   { v = bundle (\t => Either (index x.setoid t) (index y.setoid t))
-  , f = f . termToCoproduct x y
-  , g = g . termToCoproduct x y
+  , f = f . fromFree x y
+  , g = g . fromFree x y
   , cong = \x => case x of
       (Left x) => congL x
       (Right x) => congR x