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.