diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
| commit | 580970d11a4e754c0c8e6f42c8312bffb1edc2db (patch) | |
| tree | 47e85bfd18a33ed6fd87e1c82181e5cdb5f6d43b /src/Soat/FirstOrder/Algebra/Coproduct.idr | |
| parent | 242197f40bb7957625be1e5f0bfd325af6e06be4 (diff) | |
Move IsAlgebra relation from type to body.
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
| -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) |