{A B : pType} (f : A ->* B) : pfiber (pfib f) <~>* loops B. Proof. pointed_reduce_pmap f. snrapply Build_pEquiv'. 1: make_equiv_contr_basedpaths. reflexivity. Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.