forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> Tapart q1 r1 <~> Tapart q2 r2. Proof. intros ?? Eq ?? Er. apply equiv_iff_hprop_uncurried. split;apply apart_respects_aux; trivial;apply symmetry;trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.