(h : zero_object $-> a) : h $== zero_morphism := (mor_initial_unique _ _ _)^$ $@ (mor_initial_unique _ _ _).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Opposite. Require Import WildCat.Equiv.