From 4b9b6b0211f6fb5691d67ca77ac09be888e569b7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 19:25:13 +0000
Subject: Define generic syntax construction.

Whilst it works (see `Example`), a generated data type would probably
work better.
---
 src/SOAS/Algebra.idr | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/SOAS/Algebra.idr')

diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr
index 7dff735..db701d3 100644
--- a/src/SOAS/Algebra.idr
+++ b/src/SOAS/Algebra.idr
@@ -27,7 +27,6 @@ record (.MetaAlg)
 export
 traverse : {0 p,a : type.SortedFamily} ->
       {0 signature : type.SortedFunctor} ->
-      (functoriality : signature.Map) =>
       (str : Strength signature) =>
       (coalg : type.PointedCoalgStruct p) =>
       (alg : signature a -|> a) ->
-- 
cgit v1.2.3