proposition: Corollary zero_comp `{T : @Initial C} {x y : C} {f : x ~> y} : f ∘ zero ≈ zero.
proof: Proof. apply (@one_comp _ T). Qed.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Construction.Opposite