{A B : pType} (f : A ->* B) : pfiber f ->* A := Build_pMap (pfiber f) A pr1 1.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.