proposition: Lemma pfunctor_zero {A B : Type} (F : A -> B) `{IsPointedCat A, IsPointedCat B, !HasEquivs B, !Is0Functor F, !Is1Functor F, !IsPointedFunctor F} : F zero_object $<~> zero_object.
proof: Proof. rapply cate_isinitial. Defined.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv