proposition: Lemma preservation i o: Preservation sig carrier (carriers i) (λ _ v, v i) (algebra_op o) (algebra_op o).
proof: Proof. unfold product_ops, algebra_op. set (select_op := λ i0 : I, H0 i0 o). replace (H0 i o) with (select_op i) by reflexivity. clearbody select_op. revert select_op. induction (operation_type sig o). simpl. reflexivity. intros. intro. apply IHo0. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.categories.varieties