{A B : Type} (F : A -> B) `{IsPointedCat A, IsPointedCat B, !HasEquivs B, !Is0Functor F, !Is1Functor F, !IsPointedFunctor F} {a b : A} : fmap F (zero_morphism a b) $== zero_morphism (F a) (F b). Proof. refine (fmap_comp F _ _ $@ _). refine (_ $@R _ $@ _). 1: nrapply fmap_initial; [exact _]. refine (_ $@L _ $@ _). 1: nrapply fmap_terminal; [exact _]. rapply cat_zero_m. rapply pfunctor_zero. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Opposite. Require Import WildCat.Equiv.