diff options
Diffstat (limited to 'src/Soat/FirstOrder/Algebra')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 11 |
1 files changed, 7 insertions, 4 deletions
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) |