Inline definition of IsHomomorphism.

5 files changed, 129 insertions, 175 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b9c02c5..7bed448 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -53,52 +53,39 @@ public export
 (.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
 
 public export
-record IsHomomorphism
-  {0 sig : Signature} (a, b : Algebra sig)
-  (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
-  where
-  constructor MkIsHomomorphism
-  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
-    -> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
-  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-    -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
-
-public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func : IFunc a.raw.U b.raw.U
-  homo : IsHomomorphism a b func
+  func    : (t : sig.T) -> a.raw.U t -> b.raw.U t
+  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
+    -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+    -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
 
 public export
-idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
-idIsHomo = MkIsHomomorphism
-  (\_ => id)
-  (\op, tms =>
+idHomo : {a : Algebra sig} -> a ~> a
+idHomo = MkHomomorphism
+  { func    = \_ => id
+  , cong    = \_ => id
+  , semHomo = \op, tms =>
     (a.algebra.equivalence _).equalImpliesEq $
     sym $
     cong (a.raw.sem op) $
-    mapId tms)
+    mapId tms
+  }
 
 public export
-idHomo : {a : Algebra sig} -> a ~> a
-idHomo = MkHomomorphism _ idIsHomo
-
-public export
-compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
-  -> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
-compIsHomo fHomo gHomo = MkIsHomomorphism
-  (\t => fHomo.cong t . gHomo.cong t)
-  (\op, tms =>
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
+compHomo f g = MkHomomorphism
+  { func    = \t => f.func t . g.func t
+  , cong    = \t => f.cong t . g.cong t
+  , semHomo = \op, tms =>
     (c.algebra.equivalence _).transitive
-      (fHomo.cong _ $ gHomo.semHomo op tms) $
+      (f.cong _ $ g.semHomo op tms) $
     (c.algebra.equivalence _).transitive
-      (fHomo.semHomo op (map g tms)) $
+      (f.semHomo op (map g.func tms)) $
     (c.algebra.equivalence _).equalImpliesEq $
     sym $
     cong (c.raw.sem op) $
-    mapComp tms)
-
-public export
-compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
-compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
+    mapComp tms
+  }
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5e6d4ce..a98391b 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -96,28 +96,22 @@ CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
 CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
 
 public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneL
+injectLHomo : x ~> CoproductAlgebra x y
+injectLHomo = MkHomomorphism
+  { func    = \_ => Done . Left
+  , cong    = \_ => DoneL
   , semHomo = InjectL
   }
 
 public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneR
+injectRHomo : y ~> CoproductAlgebra x y
+injectRHomo = MkHomomorphism
+  { func    = \_ => Done . Right
+  , cong    = \_ => DoneR
   , semHomo = InjectR
   }
 
 public export
-injectLHomo : x ~> CoproductAlgebra x y
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
-
-public export
-injectRHomo : y ~> CoproductAlgebra x y
-injectRHomo = MkHomomorphism _ $ injectRIsHomo
-
-public export
 coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
 coproduct f g _ = bindTerm (\i => either (f i) (g i))
 
@@ -137,19 +131,19 @@ coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
   -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
 
-coproductCong f g _ (DoneL eq)       = f.homo.cong _ eq
-coproductCong f g _ (DoneR eq)       = g.homo.cong _ eq
+coproductCong f g _ (DoneL eq)       = f.cong _ eq
+coproductCong f g _ (DoneR eq)       = g.cong _ eq
 coproductCong f g _ (Call op eqs)    =
   z.algebra.semCong op $
   coproductsCong f g _ eqs
 coproductCong f g _ (InjectL op ts)  = CalcWith (z.setoid.index _) $
   |~ f.func _ (x.raw.sem op ts)
-  ~~ z.raw.sem op (map f.func ts)                                              ...(f.homo.semHomo op ts)
+  ~~ z.raw.sem op (map f.func ts)                                              ...(f.semHomo op ts)
   ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
   ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
 coproductCong f g _ (InjectR op ts)  = CalcWith (z.setoid.index _) $
   |~ g.func _ (y.raw.sem op ts)
-  ~~ z.raw.sem op (map g.func ts)                                               ...(g.homo.semHomo op ts)
+  ~~ z.raw.sem op (map g.func ts)                                               ...(g.semHomo op ts)
   ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
   ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
 coproductCong f g _ (Sym eq)         = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
@@ -162,10 +156,11 @@ coproductsCong f g _ (eq :: eqs) =
   coproductCong f g _ eq :: coproductsCong f g _ eqs
 
 public export
-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
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+  -> CoproductAlgebra x y ~> z
+coproductHomo f g = MkHomomorphism
+  { func = coproduct {z = z.raw} f.func g.func
+  , cong = coproductCong f g
   , semHomo = \op, tms =>
     (z.algebra.equivalence _).equalImpliesEq $
     cong (z.raw.sem op) $
@@ -173,16 +168,12 @@ coproductIsHomo f g = MkIsHomomorphism
   }
 
 public export
-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)
   -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
      CoproductAlgebra x y
-termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
-  { cong = \t => tmRelImpliesCoprodRel
+termToCoproduct x y = MkHomomorphism
+  { func    = \_ => id
+  , cong    = \t => tmRelImpliesCoprodRel
   , semHomo = \op, tms =>
     Call op $
     coprodsRelReflexive
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index bedfe3f..f9f0879 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -170,19 +170,16 @@ bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
 bindTermsCong env = bindTermsCong' env.cong
 
 public export
-bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
-  -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
-bindIsHomo a env = MkIsHomomorphism
-  (\t, eq => bindTermCong env eq)
-  (\op, tms =>
-      a.algebra.semCong op $
-      map (\t => (a.algebra.equivalence t).equalImpliesEq) $
-      equalImpliesPwEq $
-      bindTermsIsMap {a = a.raw} env.func tms)
-
-public export
 bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
-bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
+bindHomo env = MkHomomorphism
+  { func    = \_ => bindTerm {a = a.raw} env.func
+  , cong    = \_ => bindTermCong env
+  , semHomo = \op, tms =>
+    a.algebra.semCong op $
+    map (\t => (a.algebra.equivalence t).equalImpliesEq) $
+    equalImpliesPwEq $
+    bindTermsIsMap {a = a.raw} env.func tms
+  }
 
 public export
 bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
@@ -201,9 +198,9 @@ bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
 bindUnique' f g cong (Done i)     = cong i
 bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
   |~ f.func _ (Call op ts)
-  ~~ a.raw.sem op (map f.func ts) ...( f.homo.semHomo op ts )
+  ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
   ~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
-  ~~ g.func _ (Call op ts)        ..<( g.homo.semHomo op ts )
+  ~~ g.func _ (Call op ts)        ..<( g.semHomo op ts )
 
 bindsUnique' f g cong []        = []
 bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 0ab235b..d3e1f4c 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -132,31 +132,23 @@ public export
   (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
 
 public export
-record IsHomomorphism
-  {0 sig : Signature} (a, b : Algebra sig)
-  (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
-  constructor MkIsHomomorphism
+  constructor MkHomomorphism
+  func       : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
   cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
-    -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm')
+    -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm')
   renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
-    -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
+    -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm)
   semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.relation (t, ctx)
-         (f t ctx $ a.raw.sem ctx op tms)
-         (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
+         (func t ctx $ a.raw.sem ctx op tms)
+         (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms)
   varHomo    : {t : _} -> {ctx : _} -> (i : Elem t ctx)
-    -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
+    -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i)
   substHomo  : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
     -> (tms : (\t => a.raw.U t ctx) ^ ctx')
     -> b.relation (t, ctx)
-         (f t ctx $ a.raw.subst t ctx tm tms)
-         (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)
-
-public export
-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
-  homo : IsHomomorphism a b func
+         (func t ctx $ a.raw.subst t ctx tm tms)
+         (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms)
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 831b884..4ed29cf 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -32,80 +32,78 @@ projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Alge
 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 (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 =>
+projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b
+  -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
+projectHomo f ctx = MkHomomorphism
+  { func    = \t => f.func t ctx
+  , cong    = \t => f.cong t ctx
+  , semHomo = \op, tms =>
     (b.algebra.equivalence _).transitive
       (f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) $
     b.algebra.semCong ctx (MkOp (Op op.op)) $
     map (\(_,_) => (b.algebra.equivalence _).equalImpliesEq) $
     equalImpliesPwEq $
-    mapWrap (MkPair []) tms)
-
-public export
-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)
+    mapWrap (MkPair []) tms
+  }
 
 public export
 (.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
   -> (f : ctx `Sublist` ctx')
   -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
 (.renameHomo) a f = MkHomomorphism
-  (\t => a.raw.rename t f)
-  (MkIsHomomorphism
-    (\t => a.algebra.renameCong t f)
-    (\op, tms => (a.algebra.equivalence _).transitive
-      (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
-      (a.algebra.semCong _ (MkOp (Op op.op)) $
-       map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
-       pwSym (\_ => MkSymmetric symmetric) $
-       pwTrans (\_ => MkTransitive transitive)
-         (wrapIntro $
-          mapIntro'' (\t, tm, _, Refl =>
-            cong (\f => a.raw.rename t f tm) $
-            sym $
-            uncurryCurry f) $
-          equalImpliesPwEq Refl) $
-       equalImpliesPwEq $
-       sym $
-       mapWrap (MkPair []) tms)))
+  { func    = \t => a.raw.rename t f
+  , cong    = \t => a.algebra.renameCong t f
+  , semHomo = \op, tms => (a.algebra.equivalence _).transitive
+    (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
+    (a.algebra.semCong _ (MkOp (Op op.op)) $
+     map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
+     pwSym (\_ => MkSymmetric symmetric) $
+     pwTrans (\_ => MkTransitive transitive)
+       (wrapIntro $
+        mapIntro'' (\t, tm, _, Refl =>
+          cong (\f => a.raw.rename t f tm) $
+          sym $
+          uncurryCurry f) $
+        equalImpliesPwEq Refl) $
+     equalImpliesPwEq $
+     sym $
+     mapWrap (MkPair []) tms)
+  }
 
 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')
   -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
 (.substHomo1) a ctx tms = MkHomomorphism
-  (\t, tm => a.raw.subst t ctx tm tms)
-  (MkIsHomomorphism
-     (\t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl))
-     (\op, tms' => (a.algebra.equivalence _).transitive
-       (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
-       (a.algebra.semCong ctx (MkOp (Op op.op)) $
-        pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
-        pwTrans (\(_,_) => (a.algebra.equivalence _).trans)
-          (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
-           wrapIntro $
-           mapIntro'' (\t, tm, _, Refl =>
-             a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $
-             pwTrans (\_ => (a.algebra.equivalence _).trans)
-               (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive
-                 ((a.algebra.equivalence _).equalImpliesEq $
-                  cong (\f => a.raw.rename t f tm) $
-                  uncurryCurry reflexive)
-                 (a.algebra.renameId _ _ tm)) $
-                equalImpliesPwEq Refl) $
-             map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
-             equalImpliesPwEq $
-             mapId tms) $
-           equalImpliesPwEq Refl) $
-        map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
-        equalImpliesPwEq $
-        sym $
-        mapWrap (MkPair []) tms')))
+  { func    = \t, tm => a.raw.subst t ctx tm tms
+  , cong    = \t, eq =>
+    a.algebra.substCong t ctx eq $
+    pwRefl (\_ => (a.algebra.equivalence _).refl)
+  , semHomo = \op, tms' => (a.algebra.equivalence _).transitive
+    (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
+    (a.algebra.semCong ctx (MkOp (Op op.op)) $
+     pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
+     pwTrans (\(_,_) => (a.algebra.equivalence _).trans)
+       (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
+        wrapIntro $
+        mapIntro'' (\t, tm, _, Refl =>
+          a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $
+          pwTrans (\_ => (a.algebra.equivalence _).trans)
+            (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive
+              ((a.algebra.equivalence _).equalImpliesEq $
+               cong (\f => a.raw.rename t f tm) $
+               uncurryCurry reflexive)
+              (a.algebra.renameId _ _ tm)) $
+             equalImpliesPwEq Refl) $
+          map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
+          equalImpliesPwEq $
+          mapId tms) $
+        equalImpliesPwEq Refl) $
+     map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
+     equalImpliesPwEq $
+     sym $
+     mapWrap (MkPair []) tms')
+  }
 
 renameBodyFunc : (f : ctx `Sublist` ctx')
   -> IFunction
@@ -271,23 +269,17 @@ InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
 InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig)
 
 public export
-freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
-  -> IsHomomorphism {sig = sig}
-       (FreeAlgebra (isetoid (flip Elem ctx)))
-       (projectAlgebra sig (InitialAlgebra sig) ctx)
-       (\_ => Basics.id)
-freeToInitialIsHomo sig ctx = MkIsHomomorphism
-  (\_ => id)
-  (\(MkOp op), tms =>
+freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
+  -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
+freeToInitialHomo sig ctx = MkHomomorphism
+  { func    = \_ => id
+  , cong    = \_ => id
+  , semHomo = \(MkOp op), tms =>
     Call' (MkOp op) $
     tmsRelSym (\_ => MkSymmetric symmetric) $
     tmsRelReflexive (\_ => MkReflexive reflexive) $
-    transitive (unwrapWrap _ _) (mapId tms))
-
-public export
-freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
-  -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
-freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
+    transitive (unwrapWrap _ _) (mapId tms)
+  }
 
 public export
 fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T)
@@ -295,9 +287,9 @@ fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) ->
 fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
 
 public export
-fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
-  -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
-fromInitialIsHomo a = MkIsHomomorphism
+fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a
+fromInitialHomo a = MkHomomorphism
+  (fromInitial a.raw)
   (\t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx))
   (\t, f => bindUnique'
     {v = isetoid (flip Elem _)}
@@ -338,11 +330,6 @@ fromInitialIsHomo a = MkIsHomomorphism
     tm)
 
 public export
-fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
-  -> InitialAlgebra sig ~> a
-fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
-
-public export
 fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
   -> (f : InitialAlgebra sig ~> a)
   -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
@@ -352,4 +339,4 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
   {a = projectAlgebra sig a ctx}
   (a.varFunc ctx)
   (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
-  f.homo.varHomo
+  f.varHomo