summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Algebra/Coproduct.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 548beed..041d650 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -93,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
public export
CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
+CoproductAlgebra x y = MakeAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
public export
injectLHomo : x ~> CoproductAlgebra x y