diff options
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 84ac436..736dc75 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -17,11 +17,11 @@ CoproductSet : (0 sig : Signature) -> (0 x, y : sig.T -> Type) -> sig.T -> Type CoproductSet sig x y = Term sig (\i => Either (x i) (y i)) public export -data (~=~) : (0 x, y : RawAlgebraWithRelation sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where - DoneL : {0 x, y : RawAlgebraWithRelation sig} +data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where + DoneL : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {i, j : x.raw.U t} -> x.relation t i j -> (~=~) x y t (Done $ Left i) (Done $ Left j) - DoneR : {0 x, y : RawAlgebraWithRelation sig} + DoneR : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {i, j : y.raw.U t} -> y.relation t i j -> (~=~) x y t (Done $ Right i) (Done $ Right j) Call : {t : sig.T} -> (op : Op sig t) -> {xs, ys : _} -> Pointwise ((~=~) x y) xs ys @@ -30,12 +30,12 @@ data (~=~) : (0 x, y : RawAlgebraWithRelation sig) -> IRel (CoproductSet sig x.r -> (~=~) x y t (Done $ Left $ x.raw.sem op xs) (Call op (map (\_ => Done . Left) xs)) InjectR : {t : sig.T} -> (op : Op sig t) -> (xs : _) -> (~=~) x y t (Done $ Right $ y.raw.sem op xs) (Call op (map (\_ => Done . Right) xs)) - Sym : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm' : _} + Sym : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {tm, tm' : _} -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm - Trans : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm', tm'' : _} + Trans : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {tm, tm', tm'' : _} -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm'' -> (~=~) x y t tm tm'' -parameters {0 x, y : RawAlgebraWithRelation sig} +parameters {0 x, y : RawSetoidAlgebra sig} coprodRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation -> {t : _} -> (tm : _) -> (~=~) x y t tm tm coprodsRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation @@ -75,7 +75,7 @@ Coproduct x y = MkRawAlgebra public export CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel' -> IsAlgebra sig (Coproduct x y) - ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel')) + ((~=~) (MkRawSetoidAlgebra x rel) (MkRawSetoidAlgebra y rel')) CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra { equivalence = \t => MkEquivalence { refl = MkReflexive $ coprodRelRefl @@ -126,14 +126,14 @@ coproducts f g _ = bindTerms (\i => either (f i) (g i)) public export coproductCong : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) - -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm' + -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm' -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm' public export coproductsCong : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) -> (ts : List sig.T) -> {tms, tms' : _ ^ ts} - -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms' + -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms' -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms' coproductCong f g _ (DoneL eq) = f.homo.cong _ eq |