A = B. Proof. apply path_sigma_uncurried. destruct A as [TA [[[plA mlA] zA] uA]], B as [TB [[[plB mlB] zB] uB]];simpl in *. change plA with (@plus TA plA);change plB with (@plus TB plB); change mlA with (@mult TA mlA);change mlB with (@mult TB mlB); change zA with (@zero TA zA);change zB with (@zero TB zB); change uA with (@one TA uA);change uB with (@one TB uB). exists (path_universe f). rewrite !transport_prod;simpl. unfold Plus,Mult,Zero,One. repeat apply path_prod;simpl;try ( apply path_forall;intros x;rewrite transport_arrow; apply path_forall;intros y;rewrite transport_arrow); rewrite transport_path_universe, ?transport_path_universe_V. - rewrite (preserves_plus (f:=f)). apply ap011;apply eisretr. - rewrite (preserves_mult (f:=f)). apply ap011;apply eisretr. - apply preserves_0. - apply preserves_1. Qed.
Require Import Require Import HoTT.Classes.theory.rings.