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/Theory.idr | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

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

diff --git a/src/SOAS/Theory.idr b/src/SOAS/Theory.idr
index f36e7a1..43bb024 100644
--- a/src/SOAS/Theory.idr
+++ b/src/SOAS/Theory.idr
@@ -14,22 +14,14 @@ record (.Initial)
          (a : type.SortedFamily) where
   constructor MkInitial
   metalg : signature.MetaAlg meta a
-  bang :
+  sem :
     (0 b : type.SortedFamily) ->
-    (metalg : signature.MetaAlg meta b) ->
+    (metalg : signature.MetaAlg meta b) =>
     a -|> b
 
-public export
-(.sem) :
-  signature .Initial meta a ->
-  (0 b : type.SortedFamily) -> (metalg : signature.MetaAlg meta b) =>
-  a -|> b
-init.sem b = init.bang b metalg
-
 %hint
 public export
 (.pointedCoalgStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> type.PointedCoalgStruct a
 init.pointedCoalgStruct = MkPointedCoalgStruct
@@ -41,7 +33,6 @@ init.pointedCoalgStruct = MkPointedCoalgStruct
 %hint
 public export
 (.monStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> type.MonStruct a
 init.monStruct = MkSubstMonoidStruct
@@ -52,7 +43,6 @@ init.monStruct = MkSubstMonoidStruct
 %hint
 public export
 (.monoidStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> signature.MonoidStruct a
 init.monoidStruct = MkSignatureMonoid { mon = init.monStruct , alg = init.metalg.alg }
-- 
cgit v1.2.3