proposition: Lemma extend_inject `{Setoid A}: extend (inject A) = @id (sq A).
proof: Proof. symmetry. apply (sequence_only_extend_commutes sq); try apply _. apply sm_proper. Qed.
imports: MathClasses.theory.categories MathClasses.interfaces.functors MathClasses.interfaces.abstract_algebra MathClasses.interfaces.sequences