# theory.sequences

Require Import
theory.categories
interfaces.functors
abstract_algebra
interfaces.sequences.

Section contents.
Context `{Sequence sq}.

Lemma inject_epi `{Setoid A} `{Equiv B} `{SemiGroupOp B} `{MonoidUnit B}
(f g: sq A B) `{!Monoid_Morphism f} `{!Monoid_Morphism g} :
f inject A = g inject A f = g.

Lemma extend_comp
`{Equiv A}
`{Equiv B} `{SemiGroupOp B} `{MonoidUnit B}
`{Equiv C} `{SemiGroupOp C} `{MonoidUnit C}
(f: B C) (g: A B) `{!Monoid_Morphism f} `{!Setoid_Morphism g} :
extend (f g) (free:=sq) = f extend g (free:=sq).

Lemma extend_inject `{Setoid A}: extend (inject A) = @id (sq A).

Lemma fmap_alt `{Equiv A} `{Equiv B} (f: A B) `{!Setoid_Morphism f} :
extend (inject B f) = (fmap (v:=A) (w:=B) sq f: sq A sq B).
Lemma fold_inject `{Monoid A}: fold sq inject A = id.

Lemma fold_map `{Setoid A} `{Monoid B} (f: A B) `{!Setoid_Morphism f} :
extend f (free:=sq) = fold sq fmap (v:=A) (w:=B) sq f. End contents.

Section semiring_folds.
Context `{SemiRing R} `{Sequence sq}.

Definition sum: sq R R := @fold sq _ _ (0:R) (+).
Definition product: sq R R := @fold sq _ _ (1:R) ring_mult.

Lemma distribute_sum (a: R): (a *.) sum = sum fmap (v:=R) (w:=R) sq (a *.).
End semiring_folds.