WIP: Frex is freeHEADmaster

4 files changed, 213 insertions, 89 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 245af6d..26370cc 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -104,3 +104,11 @@ compIsHomo fHomo gHomo = MkIsHomomorphism
 public export
 compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
 compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
+
+public export
+record Isomorphism {0 sig : Signature} (a, b : Algebra sig) where
+  constructor MkIsomorphism
+  to     : Homomorphism a b
+  from   : Homomorphism b a
+  fromTo : {t : sig.T} -> (x : a.raw.U t) -> a.relation t (from.func t $ to.func t x) x
+  toFrom : {t : sig.T} -> (x : b.raw.U t) -> b.relation t (to.func t $ from.func t x) x
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index d0b1b14..a29080f 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -73,14 +73,13 @@ Coproduct x y = MakeRawAlgebra
   }
 
 public export
-CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
-  -> IsAlgebra sig (Coproduct x y)
-       ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel'))
-CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
+CoproductIsAlgebra : (x, y : Algebra sig)
+  -> IsAlgebra sig (Coproduct x.raw y.raw) ((~=~) x.rawWithRelation y.rawWithRelation)
+CoproductIsAlgebra x y = MkIsAlgebra
   { equivalence = \t => MkEquivalence
     { refl  = MkReflexive $ coprodRelRefl
-        (\t => (xIsAlgebra.equivalence t).refl)
-        (\t => (yIsAlgebra.equivalence t).refl)
+        (\t => (x.algebra.equivalence t).refl)
+        (\t => (y.algebra.equivalence t).refl)
         _
     , sym   = MkSymmetric $ Sym
     , trans = MkTransitive $ Trans
@@ -90,44 +89,88 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
 
 public export
 CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra
-
-public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneL
-  , semHomo = InjectL
-  }
-
-public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneR
-  , semHomo = InjectR
-  }
+CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x y
 
 public export
 injectLHomo : Homomorphism x (CoproductAlgebra x y)
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
+injectLHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneL , semHomo = InjectL }
 
 public export
 injectRHomo : Homomorphism y (CoproductAlgebra x y)
-injectRHomo = MkHomomorphism _ $ injectRIsHomo
+injectRHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneR , semHomo = InjectR }
 
 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))
+coproduct f g = bindTerm (\i => either (f i) (g i))
 
 public export
 coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
   -> CoproductSet sig x y ^ ts -> z.U ^ ts
-coproducts f g _ = bindTerms (\i => either (f i) (g i))
+coproducts f g = bindTerms (\i => either (f i) (g i))
+
+public export
+coproductCong' : {x, y, z : Algebra sig}
+  -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z)
+  -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j
+        -> z.relation t (f.func t i) (f'.func t j))
+  -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j
+        -> z.relation t (g.func t i) (g'.func t j))
+  -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
+  -> z.relation t
+       (coproduct {z = z.raw} f.func g.func t tm)
+       (coproduct {z = z.raw} f'.func g'.func t tm')
+
+public export
+coproductsCong' : {x, y, z : Algebra sig}
+  -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z)
+  -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j
+        -> z.relation t (f.func t i) (f'.func t j))
+  -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j
+        -> z.relation t (g.func t i) (g'.func t j))
+  -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
+  -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms'
+  -> Pointwise z.relation
+       (coproducts {z = z.raw} f.func g.func ts tms)
+       (coproducts {z = z.raw} f'.func g'.func ts tms')
+
+coproductCong' f f' g g' congL congR _ (DoneL eq)       = congL _ eq
+coproductCong' f f' g g' congL congR _ (DoneR eq)       = congR _ eq
+coproductCong' f f' g g' congL congR _ (Call op eqs)    =
+  z.algebra.semCong op $
+  coproductsCong' f f' g g' congL congR _ eqs
+coproductCong' f f' g g' congL congR _ (InjectL op ts)  = CalcWith (z.setoid.index _) $
+  |~ f.func _ (x.raw.sem op ts)
+  ~~ f'.func _ (x.raw.sem op ts)                                                 ...(congL _ $ (x.algebra.equivalence _).reflexive {x = x.raw.sem op ts})
+  ~~ z.raw.sem op (map f'.func ts)                                               ...(f'.homo.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 f' g g' congL congR _ (InjectR op ts)  = CalcWith (z.setoid.index _) $
+  |~ g.func _ (y.raw.sem op ts)
+  ~~ g'.func _ (y.raw.sem op ts)                                                  ...(congR _ $ (y.algebra.equivalence _).reflexive {x = y.raw.sem op ts})
+  ~~ z.raw.sem op (map g'.func ts)                                                ...(g'.homo.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 f' g g' congL congR _ (Sym eq)         =
+  (z.algebra.equivalence _).symmetric $
+  coproductCong' f' f g' g
+    (\t => (z.algebra.equivalence t).symmetric . congL t . (x.algebra.equivalence t).symmetric)
+    (\t => (z.algebra.equivalence t).symmetric . congR t . (y.algebra.equivalence t).symmetric)
+    _
+    eq
+coproductCong' f f' g g' congL congR _ (Trans eq eq')   = (z.algebra.equivalence _).transitive
+  (coproductCong' f f g g f.homo.cong g.homo.cong _ eq)
+  (coproductCong' f f' g g' congL congR _ eq')
+
+coproductsCong' f f' g g' congL congR _ []          = []
+coproductsCong' f f' g g' congL congR _ (eq :: eqs) =
+  coproductCong' f f' g g' congL congR _ eq :: coproductsCong' f f' g g' congL congR _ eqs
 
 public export
 coproductCong : {x, y, z : Algebra sig}
   -> (f : Homomorphism x z) -> (g : Homomorphism y z)
   -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
   -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
+coproductCong f g = coproductCong' f f g g f.homo.cong g.homo.cong
 
 public export
 coproductsCong : {x, y, z : Algebra sig}
@@ -135,30 +178,7 @@ coproductsCong : {x, y, z : Algebra sig}
   -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
   -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) 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 _ (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 (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 (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
-coproductCong f g _ (Trans eq eq')   = (z.algebra.equivalence _).transitive
-  (coproductCong f g _ eq)
-  (coproductCong f g _ eq')
-
-coproductsCong f g _ []          = []
-coproductsCong f g _ (eq :: eqs) =
-  coproductCong f g _ eq :: coproductsCong f g _ eqs
+coproductsCong f g = coproductsCong' f f g g f.homo.cong g.homo.cong
 
 public export
 coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
diff --git a/src/Soat/FirstOrder/Algebra/FreeExtension.idr b/src/Soat/FirstOrder/Algebra/FreeExtension.idr
new file mode 100644
index 0000000..675c65b
--- /dev/null
+++ b/src/Soat/FirstOrder/Algebra/FreeExtension.idr
@@ -0,0 +1,58 @@
+module Soat.FirstOrder.Algebra.FreeExtension
+
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
+
+import Soat.FirstOrder.Algebra
+import Soat.FirstOrder.Algebra.Coproduct
+import Soat.FirstOrder.Signature
+import Soat.FirstOrder.Term
+
+%default total
+
+public export
+FreeExtension : (a : RawAlgebra sig) -> (v : sig.T -> Type) -> RawAlgebra sig
+FreeExtension a v = Coproduct a (Free v)
+
+public export
+FreeExtensionAlgebra : (a : Algebra sig) -> (v : ISetoid sig.T) -> Algebra sig
+FreeExtensionAlgebra a v = CoproductAlgebra a (FreeAlgebra v)
+
+public export
+extend : {a : RawAlgebra sig} -> {u : sig.T -> Type} -> (f : IFunc v u)
+  -> IFunc (FreeExtension a v).U (FreeExtension a u).U
+extend f = coproduct {z = FreeExtension a u}
+  (\_ => Done . Left)
+  (\t => Done . Right . free f t)
+
+public export
+extendHomo : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
+  -> Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u)
+extendHomo f = coproductHomo {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))
+
+public export
+extendCong : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
+  -> (t : sig.T) -> {tm, tm' : (FreeExtension a.raw v.U).U t}
+  -> (FreeExtensionAlgebra a v).relation t tm tm'
+  -> ((FreeExtensionAlgebra a u).relation t `on` extend {a = a.raw} f.func t) tm tm'
+extendCong f = coproductCong {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))
+
+public export
+extendUnique : {a : Algebra sig} -> {v, u : ISetoid sig.T}
+  -> (f : IFunction v u)
+  -> (g : Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u))
+  -> (congL : {t : sig.T} -> (i : a.raw.U t)
+        -> (FreeExtensionAlgebra a u).relation t (g.func t (Done (Left i))) (Done (Left i)))
+  -> (congR : {t : sig.T} -> (i : Term sig v.U t)
+        -> (FreeExtensionAlgebra a u).relation t
+             (g.func t (Done (Right i)))
+             (Done (Right (free f.func t i))))
+  -> {t : sig.T} -> (tm : _)
+  -> (FreeExtensionAlgebra a u).relation t (g.func t tm) (extend {a = a.raw} f.func t tm)
+extendUnique f = coproductUnique {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..dc0c182 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -15,25 +15,6 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
   Done : (i : v t) -> Term sig v t
   Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
 
-public export
-bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t
-
-public export
-bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
-
-bindTerm         env (Done i)     = env _ i
-bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
-
-bindTerms env []        = []
-bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
-
-public export
-bindTermsIsMap : {auto a : RawAlgebra sig}
-  -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
-  -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
-bindTermsIsMap env []        = Refl
-bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
-
 -- FIXME: these names shouldn't be public. Indication of bad API design
 namespace Rel
   public export
@@ -138,42 +119,85 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig
 FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
 
 public export
+inject : IFunc v (Term sig v)
+inject _ = Done
+
+public export
+injectFunc : IFunction v (FreeAlgebra v).setoid
+injectFunc = MkIFunction (\_ => Done) (\_ => Done')
+
+public export
+bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc (Term sig v) a.U
+
+public export
+bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc ((^) (Term sig v)) ((^) a.U)
+
+bindTerm env _ (Done i)     = env _ i
+bindTerm env _ (Call op ts) = a.sem op (bindTerms env _ ts)
+
+bindTerms env _ []        = []
+bindTerms env _ (t :: ts) = bindTerm env _ t :: bindTerms env _ ts
+
+public export
+free : IFunc v u -> IFunc (Term sig v) (Term sig u)
+free f = bindTerm {a = Free u} (\i => inject i . f i)
+
+public export
+bindTermsIsMap : {a : RawAlgebra sig}
+  -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
+  -> bindTerms (\tm => env tm) _ tms = map (bindTerm (\tm => env tm)) tms
+bindTermsIsMap env []        = Refl
+bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env _ t)) (bindTermsIsMap env ts)
+
+public export
 bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
   -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-  -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
-  -> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
+  -> (t : sig.T) -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
+  -> a.relation t (bindTerm {a = a.raw} env t tm) (bindTerm {a = a.raw} env' t tm')
 
 public export
 bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
   -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-  -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
-  -> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
+  -> (ts : List sig.T) -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
+  -> Pointwise a.relation (bindTerms {a = a.raw} env _ tms) (bindTerms {a = a.raw} env' _ tms')
 
-bindTermCong'         cong (Done' i)     = cong _ i
-bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
+bindTermCong' cong _ (Done' i)     = cong _ i
+bindTermCong' cong _ (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong _ ts)
 
-bindTermsCong' cong []        = []
-bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
+bindTermsCong' cong _ []        = []
+bindTermsCong' cong _ (t :: ts) = bindTermCong' cong _ t :: bindTermsCong' cong _ ts
+
+public export
+freeCong' : {u : ISetoid sig.T} -> {f, g : IFunc v u.U} -> {0 rel : IRel v}
+  -> (cong : (t : sig.T) -> {i, j : v t} -> rel t i j -> u.relation t (f t i) (g t j))
+  -> (t : sig.T) -> {tm, tm' : Term sig v t}
+  -> (~=~) rel t tm tm' -> (~=~) u.relation t (free f t tm) (free g t tm')
+freeCong' cong = bindTermCong' {a = FreeAlgebra u} (\i => Done' . cong i)
 
 public export
 bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
-  -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
+  -> (t : sig.T) -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
+  -> a.relation t (bindTerm {a = a.raw} env.func t tm) (bindTerm {a = a.raw} env.func t tm')
 bindTermCong env = bindTermCong' env.cong
 
 public export
 bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
+  -> (ts : List sig.T) -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
   -> Pointwise a.relation
-       (bindTerms {a = a.raw} env.func tms)
-       (bindTerms {a = a.raw} env.func tms')
+       (bindTerms {a = a.raw} env.func ts tms)
+       (bindTerms {a = a.raw} env.func ts tms')
 bindTermsCong env = bindTermsCong' env.cong
 
 public export
+freeCong : {u : ISetoid sig.T} -> (f : IFunction v u) -> (t : sig.T) -> {tm, tm' : Term sig v.U t}
+  -> (~=~) v.relation t tm tm' -> (~=~) u.relation t (free f.func t tm) (free f.func t tm')
+freeCong f = freeCong' f.cong
+
+public export
 bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
-  -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
+  -> IsHomomorphism (FreeAlgebra v) a (bindTerm {a = a.raw} env.func)
 bindIsHomo a env = MkIsHomomorphism
-  (\t, eq => bindTermCong env eq)
+  (bindTermCong env)
   (\op, tms =>
       a.algebra.semCong op $
       map (\t => (a.algebra.equivalence t).equalImpliesEq) $
@@ -185,14 +209,19 @@ bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (Fr
 bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
 
 public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+freeHomo : {u : ISetoid sig.T} -> IFunction v u
+  -> Homomorphism {sig = sig} (FreeAlgebra v) (FreeAlgebra u)
+freeHomo f = bindHomo $ compFunc injectFunc f
+
+public export
+bindUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig}
   -> (f, g : Homomorphism (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}
+bindsUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig}
   -> (f, g : Homomorphism (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)
@@ -213,7 +242,7 @@ bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.se
   -> (f : Homomorphism (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)
+  -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func t tm)
 bindUnique env f = bindUnique' f (bindHomo env)
 
 public export
@@ -221,8 +250,17 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s
   -> (f : Homomorphism (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)
+  -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func ts tms)
 bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $
   |~ map f.func ts
-  ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
-  ~~ bindTerms {a = a.raw} env.func ts            .=<( bindTermsIsMap {a = a.raw} env.func ts )
+  ~~ map (bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
+  ~~ bindTerms {a = a.raw} env.func _ ts    .=<( bindTermsIsMap {a = a.raw} env.func ts )
+
+public export
+freeUnique : {v, u : ISetoid sig.T} -> (f : IFunction v u)
+  -> (g : Homomorphism (FreeAlgebra v) (FreeAlgebra u))
+  -> (cong : {t : sig.T} -> (i : v.U t)
+        -> (FreeAlgebra u).relation t (g.func t (Done i)) (Done (f.func t i)))
+  -> {t : sig.T} -> (tm : Term sig v.U t)
+  -> (FreeAlgebra u).relation t (g.func t tm) (free f.func t tm)
+freeUnique f = bindUnique $ compFunc injectFunc f