diff options
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 29a740f..5e6d4ce 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -110,11 +110,11 @@ injectRIsHomo = MkIsHomomorphism } public export -injectLHomo : Homomorphism x (CoproductAlgebra x y) +injectLHomo : x ~> CoproductAlgebra x y injectLHomo = MkHomomorphism _ $ injectLIsHomo public export -injectRHomo : Homomorphism y (CoproductAlgebra x y) +injectRHomo : y ~> CoproductAlgebra x y injectRHomo = MkHomomorphism _ $ injectRIsHomo public export @@ -127,14 +127,12 @@ coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _) 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) +coproductCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z) -> (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) +coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z) -> (ts : List sig.T) -> {tms, tms' : _ ^ ts} -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms' -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms' @@ -164,7 +162,7 @@ coproductsCong f g _ (eq :: eqs) = coproductCong f g _ eq :: coproductsCong f g _ eqs public export -coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) +coproductIsHomo : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z) -> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func) coproductIsHomo f g = MkIsHomomorphism { cong = coproductCong f g @@ -175,15 +173,14 @@ coproductIsHomo f g = MkIsHomomorphism } public export -coproductHomo : {x, y, z : Algebra sig} -> Homomorphism x z -> Homomorphism y z - -> Homomorphism (CoproductAlgebra x y) z +coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z + -> CoproductAlgebra x y ~> z coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g public export termToCoproduct : (x, y : Algebra sig) - -> Homomorphism - (FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i)))) - (CoproductAlgebra x y) + -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~> + CoproductAlgebra x y termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism { cong = \t => tmRelImpliesCoprodRel , semHomo = \op, tms => @@ -197,8 +194,8 @@ termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism public export coproductUnique' : {x, y, z : Algebra sig} - -> (f : Homomorphism (CoproductAlgebra x y) z) - -> (g : Homomorphism (CoproductAlgebra x y) z) + -> (f : CoproductAlgebra x y ~> z) + -> (g : CoproductAlgebra x y ~> z) -> (congL : {t : sig.T} -> (i : x.raw.U t) -> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i)))) -> (congR : {t : sig.T} -> (i : y.raw.U t) @@ -216,8 +213,8 @@ coproductUnique' f g congL congR tm = bindUnique' } public export -coproductUnique : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) - -> (h : Homomorphism (CoproductAlgebra x y) z) +coproductUnique : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z) + -> (h : CoproductAlgebra x y ~> z) -> (congL : {t : sig.T} -> (i : x.raw.U t) -> z.relation t (h.func t (Done (Left i))) (f.func t i)) -> (congR : {t : sig.T} -> (i : y.raw.U t) |