proposition: 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: Proof. 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.
imports: MathClasses.theory.categories MathClasses.interfaces.functors MathClasses.interfaces.abstract_algebra MathClasses.interfaces.sequences