(n : trunc_index) {F X Y : pType} (i : F ->* X) (f : X ->* Y) (cx : IsComplex i f) : IsComplex (fmap (pTr n) i) (fmap (pTr n) f). Proof. refine ((fmap_comp (pTr n) i f)^* @* _). refine (_ @* ptr_functor_pconst n). rapply (fmap2 (pTr _)); assumption. 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.