Library MathClasses.theory.sequences

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

Section contents.
  Context `{Sequence sq}.

  Lemma inject_epi `{Setoid A} `{Equiv B} `{SgOp B} `{MonUnit B}
    (f g: sq A → B) `{!Monoid_Morphism f} `{!Monoid_Morphism g} :
      f ∘ inject A = g ∘ inject A → f = g.
  Proof with intuition.
   intros.
   pose proof (setoidmor_a f).
   pose proof (monmor_b (f:=g)).
   pose proof (sequence_only_extend_commutes sq (f ∘ inject A) _) as E.
   pose proof (_ : Setoid_Morphism (f ∘ inject A)) as cm.
   rewrite (E f), (E g)...
    apply (sequence_extend_morphism sq)...
    apply cm.
   apply cm.
  Qed.

  Lemma extend_comp
    `{Equiv A}
    `{Equiv B} `{SgOp B} `{MonUnit B}
    `{Equiv C} `{SgOp C} `{MonUnit C}
     (f: B → C) (g: A → B) `{!Monoid_Morphism f} `{!Setoid_Morphism g} :
    extend (f ∘ g) (free:=sq) = f ∘ extend g (free:=sq).
  Proof with try apply _.
   intros.
   pose proof (setoidmor_a g).
   pose proof (monmor_a (f:=f)).
   pose proof (monmor_b (f:=f)).
   symmetry.
   apply (sequence_only_extend_commutes sq (f ∘ g))...
   symmetry.
   rewrite <- (sequence_extend_commutes sq g _) at 1.
   apply sm_proper.
  Qed.

  Lemma extend_inject `{Setoid A}: extend (inject A) = @id (sq A).
  Proof.
   symmetry. apply (sequence_only_extend_commutes sq); try apply _.
   apply sm_proper.
  Qed.


  Lemma fold_inject `{Monoid A}: fold sq ∘ inject A = id.
  Proof. apply (sequence_extend_commutes sq id). apply _. Qed.

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) mult.

End semiring_folds.