From 580970d11a4e754c0c8e6f42c8312bffb1edc2db Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 5 Dec 2022 15:00:39 +0000 Subject: Move IsAlgebra relation from type to body. --- src/Soat/FirstOrder/Algebra/Coproduct.idr | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/Soat/FirstOrder/Algebra') diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 736dc75..29a740f 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -73,11 +73,14 @@ Coproduct x y = MkRawAlgebra } public export -CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel' +CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y -> IsAlgebra sig (Coproduct x y) - ((~=~) (MkRawSetoidAlgebra x rel) (MkRawSetoidAlgebra y rel')) CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra - { equivalence = \t => MkEquivalence + { relation = + (~=~) + (MkRawSetoidAlgebra x xIsAlgebra.relation) + (MkRawSetoidAlgebra y yIsAlgebra.relation) + , equivalence = \t => MkEquivalence { refl = MkReflexive $ coprodRelRefl (\t => (xIsAlgebra.equivalence t).refl) (\t => (yIsAlgebra.equivalence t).refl) @@ -90,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra public export CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig -CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra +CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra public export injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left) -- cgit v1.2.3