{A B : Type} (F : A -> B) `{IsPointedCat A, IsPointedCat B, !HasEquivs B, !HasMorExt B} `{!Is0Functor F, !Is1Functor F, !IsPointedFunctor F} {a1 a2 : A} : pHom a1 a2 ->* pHom (F a1) (F a2). Proof. snrapply Build_pMap. - exact (fmap F). - apply path_hom. snrapply fmap_zero_morphism; assumption. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.