q r : (' q) + (' r) = ' (PairT.pl _ q r) := 1. Global Instance Z_mult@{} : Mult Z. Proof. refine (Z_rec2 (fun x y => ' (PairT.ml@{UN UNalt} _ x y)) _). intros;apply Z_path;eapply PairT.ml_respects;trivial. Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.