Z_to_ring_unique@{} `{IsCRing B} (h : Z -> B) `{!IsSemiRingPreserving h} : forall x : Z, integers_to_ring Z B x = h x. Proof. pose proof Z_ring. apply (Z_ind _). intros [pa na];unfold integers_to_ring;simpl. rewrite Npair_splits. rewrite (preserves_plus (f:=h)),(preserves_negate (f:=h)). change (h (' pa)) with (Compose h (cast N Z) pa). change (h (' na)) with (Compose h (cast N Z) na). rewrite 2!(naturals_initial (h:=Compose h (cast N Z))). trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.