`{Univalence} (n : trunc_index) (A : pType) : (ptr_loops n A) o* ptr ==* fmap loops ptr. Proof. srapply Build_pHomotopy. - intro p. simpl. refine (_ @ _). + apply path_Tr_commutes. + symmetry; refine (_ @ _). * apply concat_1p. * apply concat_p1. - simpl. reflexivity. Defined.
Require Import Basics Types WildCat Truncations