diff options
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 2042d2f..a53e6b0 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -105,17 +105,20 @@ namespace Rel , transitive = \t, x, y, z => tmRelTrans eq.transitive } + public export + Term : (0 sig : Signature) -> (V : IndexedSetoid sig.T) -> IndexedSetoid sig.T + Term sig v = MkIndexedSetoid (Term sig v.U) (tmRelEq v.equivalence) + public export Free : (0 V : sig.T -> Type) -> RawAlgebra sig Free v = MkRawAlgebra (Term sig v) Call public export -FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U) -FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call - -public export FreeAlgebra : IndexedSetoid sig.T -> Algebra sig -FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v) +FreeAlgebra v = MkAlgebra + { U = Term sig v + , sem = \op => MkSetoidHomomorphism (Call op) (\_, _ => Call op) + } public export bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t} |