refactor: rename Homomorphism -> (~>).

1 files changed, 13 insertions, 16 deletions

diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 29a740f..5e6d4ce 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -110,11 +110,11 @@ injectRIsHomo = MkIsHomomorphism
   }
 
 public export
-injectLHomo : Homomorphism x (CoproductAlgebra x y)
+injectLHomo : x ~> CoproductAlgebra x y
 injectLHomo = MkHomomorphism _ $ injectLIsHomo
 
 public export
-injectRHomo : Homomorphism y (CoproductAlgebra x y)
+injectRHomo : y ~> CoproductAlgebra x y
 injectRHomo = MkHomomorphism _ $ injectRIsHomo
 
 public export
@@ -127,14 +127,12 @@ coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
 coproducts f g _ = bindTerms (\i => either (f i) (g i))
 
 public export
-coproductCong : {x, y, z : Algebra sig}
-  -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
   -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
 
 public export
-coproductsCong : {x, y, z : Algebra sig}
-  -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
   -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
   -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
@@ -164,7 +162,7 @@ coproductsCong f g _ (eq :: eqs) =
   coproductCong f g _ eq :: coproductsCong f g _ eqs
 
 public export
-coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductIsHomo : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func)
 coproductIsHomo f g = MkIsHomomorphism
   { cong = coproductCong f g
@@ -175,15 +173,14 @@ coproductIsHomo f g = MkIsHomomorphism
   }
 
 public export
-coproductHomo : {x, y, z : Algebra sig} -> Homomorphism x z -> Homomorphism y z
-  -> Homomorphism (CoproductAlgebra x y) z
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+  -> CoproductAlgebra x y ~> z
 coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g
 
 public export
 termToCoproduct : (x, y : Algebra sig)
-  -> Homomorphism
-       (FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))))
-       (CoproductAlgebra x y)
+  -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
+     CoproductAlgebra x y
 termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
   { cong = \t => tmRelImpliesCoprodRel
   , semHomo = \op, tms =>
@@ -197,8 +194,8 @@ termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
 
 public export
 coproductUnique' : {x, y, z : Algebra sig}
-  -> (f : Homomorphism (CoproductAlgebra x y) z)
-  -> (g : Homomorphism (CoproductAlgebra x y) z)
+  -> (f : CoproductAlgebra x y ~> z)
+  -> (g : CoproductAlgebra x y ~> z)
   -> (congL : {t : sig.T} -> (i : x.raw.U t)
         -> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i))))
   -> (congR : {t : sig.T} -> (i : y.raw.U t)
@@ -216,8 +213,8 @@ coproductUnique' f g congL congR tm = bindUnique'
   }
 
 public export
-coproductUnique : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
-  -> (h : Homomorphism (CoproductAlgebra x y) z)
+coproductUnique : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
+  -> (h : CoproductAlgebra x y ~> z)
   -> (congL : {t : sig.T} -> (i : x.raw.U t)
         -> z.relation t (h.func t (Done (Left i))) (f.func t i))
   -> (congR : {t : sig.T} -> (i : y.raw.U t)