`{DecidablePaths N} : forall q r : PairT.T N, Decidable (' q = ' r). Proof. intros q r. destruct (dec (PairT.equiv q r)) as [E|E]. - left. apply Z_path,E. - right. intros E'. apply E. apply (related_path E'). Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.