`{Univalence} (n : nat) (X : pType) : IsEquiv (fmap (pPi n) ptr : Pi n X -> Pi n (pTr n X)) := _.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.