{A B : pType} (f : A ->* B) : pType := [hfiber f (point B), _].
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.