diff options
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 10 |
1 files changed, 5 insertions, 5 deletions
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) |