PropositionsForAdditiveCategories.tex

\begin{sequent}
\begin{align*}
   a: \Obj ~|~ \IsZero \big( a \big) \vdash \IsZero \big( \IdentityMorphism( a ) \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
   a: \Obj, b: \Obj ~|~ \IsZero \big( a \big), \IsZero \big( b \big) \\
   \vdash & \IsZero \big( \DirectSum( [ a, b ] ) \big)
\end{align*}
\end{sequent}