fact: Definition ZeroMaps (C:category) := ∑ (zero : ∏ a b:C, a --> b), (∏ a b c, ∏ f:b --> c, f ∘ zero a b = zero a c) × (∏ a b c, ∏ f:c --> b, zero b a ∘ f = zero c a).
imports: UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.Foundations.Preamble UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics