refactor: rename Homomorphism -> (~>).

5 files changed, 42 insertions, 44 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6f9389b..b9c02c5 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -8,6 +8,8 @@ import Soat.FirstOrder.Signature
 %default total
 %hide Control.Relation.Equivalence
 
+infix 5 ~>
+
 public export 0
 algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
 algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
@@ -62,7 +64,7 @@ record IsHomomorphism
     -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
 
 public export
-record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
   func : IFunc a.raw.U b.raw.U
@@ -79,7 +81,7 @@ idIsHomo = MkIsHomomorphism
     mapId tms)
 
 public export
-idHomo : {a : Algebra sig} -> Homomorphism a a
+idHomo : {a : Algebra sig} -> a ~> a
 idHomo = MkHomomorphism _ idIsHomo
 
 public export
@@ -98,5 +100,5 @@ compIsHomo fHomo gHomo = MkIsHomomorphism
     mapComp tms)
 
 public export
-compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
 compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
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)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 45282cc..bedfe3f 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -181,19 +181,19 @@ bindIsHomo a env = MkIsHomomorphism
       bindTermsIsMap {a = a.raw} env.func tms)
 
 public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a
+bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
 bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
 
 public export
 bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-  -> (f, g : Homomorphism (FreeAlgebra v) a)
+  -> (f, g : FreeAlgebra v ~> a)
   -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
   -> {t : sig.T} -> (tm : Term sig v.U t)
   -> a.relation t (f.func t tm) (g.func t tm)
 
 public export
 bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-  -> (f, g : Homomorphism (FreeAlgebra v) a)
+  -> (f, g : FreeAlgebra v ~> a)
   -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
   -> Pointwise a.relation (map f.func tms) (map g.func tms)
@@ -210,7 +210,7 @@ bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g con
 
 public export
 bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> (f : Homomorphism (FreeAlgebra v) a)
+  -> (f : FreeAlgebra v ~> a)
   -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
   -> {t : sig.T} -> (tm : Term sig v.U t)
   -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
@@ -218,7 +218,7 @@ bindUnique env f = bindUnique' f (bindHomo env)
 
 public export
 bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> (f : Homomorphism (FreeAlgebra v) a)
+  -> (f : FreeAlgebra v ~> a)
   -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
   -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 475bdc0..0ab235b 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -8,6 +8,8 @@ import Soat.Data.Product
 import Soat.Data.Sublist
 import Soat.SecondOrder.Signature
 
+infix 5 ~>
+
 public export
 extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type
 extend x ctx ty = x (snd ty) (fst ty ++ ctx)
@@ -153,7 +155,7 @@ record IsHomomorphism
          (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)
 
 public export
-record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
   func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 5f52f82..831b884 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -28,14 +28,13 @@ projectIsAlgebra a ctx = MkIsAlgebra
   (\op => a.semCong ctx _ . wrapIntro)
 
 public export
-projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
-  -> FirstOrder.Algebra.Algebra sig
-projectAlgebra a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
+projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
 
 public export
 projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
   -> (ctx : _)
-  -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx)
+  -> IsHomomorphism (projectAlgebra sig a ctx) (projectAlgebra sig b ctx) (\t => f t ctx)
 projectIsHomo {b = b} f ctx = MkIsHomomorphism
   (\t => f.cong t ctx)
   (\op, tms =>
@@ -47,14 +46,14 @@ projectIsHomo {b = b} f ctx = MkIsHomomorphism
     mapWrap (MkPair []) tms)
 
 public export
-projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b
-  -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx)
+projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b
+  -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
 projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx)
 
 public export
 (.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
   -> (f : ctx `Sublist` ctx')
-  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx')
+  -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
 (.renameHomo) a f = MkHomomorphism
   (\t => a.raw.rename t f)
   (MkIsHomomorphism
@@ -78,7 +77,7 @@ public export
 public export
 (.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T)
   -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
-  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx)
+  -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
 (.substHomo1) a ctx tms = MkHomomorphism
   (\t, tm => a.raw.subst t ctx tm tms)
   (MkIsHomomorphism
@@ -275,7 +274,7 @@ public export
 freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
   -> IsHomomorphism {sig = sig}
        (FreeAlgebra (isetoid (flip Elem ctx)))
-       (projectAlgebra (InitialAlgebra sig) ctx)
+       (projectAlgebra sig (InitialAlgebra sig) ctx)
        (\_ => Basics.id)
 freeToInitialIsHomo sig ctx = MkIsHomomorphism
   (\_ => id)
@@ -287,9 +286,7 @@ freeToInitialIsHomo sig ctx = MkIsHomomorphism
 
 public export
 freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
-  -> Homomorphism {sig = sig}
-       (FreeAlgebra (isetoid (flip Elem ctx)))
-       (projectAlgebra (InitialAlgebra sig) ctx)
+  -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
 freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
 
 public export
@@ -301,10 +298,10 @@ public export
 fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
   -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
 fromInitialIsHomo a = MkIsHomomorphism
-  (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx))
+  (\t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx))
   (\t, f => bindUnique'
     {v = isetoid (flip Elem _)}
-    {a = projectAlgebra a _}
+    {a = projectAlgebra sig a _}
     (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
     (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
     (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
@@ -321,14 +318,14 @@ fromInitialIsHomo a = MkIsHomomorphism
   (\_ => (a.algebra.equivalence _).reflexive)
   (\t, ctx, tm, tms => bindUnique'
     {v = isetoid (flip Elem _)}
-    {a = projectAlgebra a _}
+    {a = projectAlgebra sig a _}
     (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms)))
     (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
     (\i =>
       (a.algebra.equivalence _).transitive
         (bindUnique
           {v = isetoid (flip Elem _)}
-          {a = projectAlgebra a _}
+          {a = projectAlgebra sig a _}
           (a.varFunc _)
           (bindHomo (a.varFunc _))
           (\i => (a.algebra.equivalence _).reflexive)
@@ -342,17 +339,17 @@ fromInitialIsHomo a = MkIsHomomorphism
 
 public export
 fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
-  -> Homomorphism (InitialAlgebra sig) a
+  -> InitialAlgebra sig ~> a
 fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
 
 public export
 fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
-  -> (f : Homomorphism (InitialAlgebra sig) a)
+  -> (f : InitialAlgebra sig ~> a)
   -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
   -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
 fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
   {v = isetoid (flip Elem _)}
-  {a = projectAlgebra a ctx}
+  {a = projectAlgebra sig a ctx}
   (a.varFunc ctx)
   (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
   f.homo.varHomo