proposition: Lemma integer_initial (same_morphism : ∀ `{Ring B} {h : A → B} `{!SemiRing_Morphism h}, integers_to_ring B = h) : Initial (rings.object A).
proof: Proof. intros y [x h] [] ?. simpl in *. apply same_morphism. apply rings.decode_variety_and_ops. apply (@rings.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). reflexivity. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories MathClasses.categories.varieties