refactor: rename Homomorphism.f -> func.

3 files changed, 12 insertions, 12 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index bbc0430..5428ca3 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -60,5 +60,5 @@ public export
 record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  f    : (t : sig.T) -> a.raw.U t -> b.raw.U t
-  homo : IsHomomorphism a b f
+  func : IFunc a.raw.U b.raw.U
+  homo : IsHomomorphism a b func
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 92f35cc..e39e7ac 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -157,16 +157,16 @@ bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
 public export
 bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
   -> (f, g : Homomorphism (FreeAlgebra v) a)
-  -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (g.f t (Done i)))
+  -> ({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.f t tm) (g.f t tm)
+  -> 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)
-  -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (g.f t (Done i)))
+  -> ({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.f tms) (map g.f tms)
+  -> Pointwise a.relation (map f.func tms) (map g.func tms)
 
 bindUnique' f g cong (Done i)     = cong i
 bindUnique' f g cong (Call op ts) =
@@ -183,17 +183,17 @@ 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)
-  -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (env.func t i))
+  -> ({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.f t tm) (bindTerm {a = a.raw} env.func tm)
+  -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
 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)
-  -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (env.func t i))
+  -> ({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.f tms) (bindTerms {a = a.raw} env.func tms)
+  -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
 bindsUnique env f cong ts =
   pwTrans (\i => (a.algebra.equivalence i).trans)
     (bindsUnique' f (bindHomo env) cong ts) $
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 57b8a51..5457385 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -138,5 +138,5 @@ public export
 record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  f    : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
-  homo : IsHomomorphism a b f
+  func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
+  homo : IsHomomorphism a b func