From fcd024cb01e484dc3c92212f4317b254bbd7580b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 6 Dec 2022 16:18:29 +0000
Subject: Add smart constructor for first-order algebras.

---
 src/Soat/SecondOrder/Algebra/Lift.idr | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')

diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index d80eeb1..8bbcf9e 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -26,11 +26,10 @@ project a ctx = MkRawAlgebra
 public export
 projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
 projectAlgebra sig a ctx = MkAlgebra
-  { raw = project a.raw ctx
-  , algebra = MkIsAlgebra
-    { equivalence = (reindex (flip MkPair ctx) a.setoid).equivalence
-    , semCong     = \op => a.algebra.semCong ctx (MkOp (Op op.op)) . wrapIntro
-    }
+  { U   = a.setoidAt ctx
+  , sem = \op =>
+    a.semFunc ctx (MkOp (Op op.op)) .
+    index (wrapFunc (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) (MkPair [])) _
   }
 
 public export
-- 
cgit v1.2.3