fact: Definition pfmap {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).
imports: Basics Types PathAny WildCat Truncations.Core ReflectiveSubuniverse Extensions