{n A} (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} : (forall a, P (tr a)) -> (forall aa, P aa) := fun f aa => match aa with tr a => fun _ => f a end Pt.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.