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