{Y : pType} (P : pFam Y) : loops Y ->* [P pt, dpoint P]. Proof. srapply Build_pMap. - intro l. apply (transport P l). apply P. - reflexivity. Defined.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.