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