g $o zero_morphism a b $== zero_morphism a c. Proof. refine ((_ $@R _) $@ cat_assoc _ _ _)^$. apply mor_initial_unique. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Opposite. Require Import WildCat.Equiv.