{X Y : pType} (f : X ->* Y) : IsComplex (@pconst pUnit X) f. Proof. srapply Build_pHomotopy. - intro x; cbn. exact (point_eq f). - cbn; symmetry. exact (concat_p1 _ @ concat_1p _). 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.