proposition: Lemma ZeroArrowEq (Z : Zero) (a b : C) (f1 : C⟦a, Z⟧) (g1 : C⟦Z, b⟧) : f1 · g1 = ZeroArrow Z a b.
proof: Proof. rewrite (ArrowsToZero Z a f1 (ZeroArrowTo Z a)). rewrite (ArrowsFromZero Z b g1 (ZeroArrowFrom Z b)). apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal