`{Univalence} (n : trunc_index) (A : pType) : pTr n (loops A) <~>* loops (pTr n.+1 A). Proof. srapply Build_pEquiv'. 1: apply equiv_path_Tr. reflexivity. Defined.
Require Import Basics Types WildCat Truncations