Quelle  RelationsForGeneralCategories.tex

\begin{sequent}
\begin{align*}
  &t, \alpha:\Mor\\
  |~ &\IsZeroForMorphisms\big( \PreCompose( t, \alpha ) \big)\\
  \vdash &\PreCompose\big(\KernelLift( \alpha , t ), \KernelEmbedding( \alpha ) \big) =_{\Mor} t
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &t, \alpha:\Mor\\
  |~  &\IsZeroForMorphisms\big(\PreCompose(\alpha, t)\big)\\
  \vdash &\PreCompose\big(\CokernelProjection( \alpha ), \CokernelColift( \alpha, t )\big) =_{\Mor} t
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &L:\ListObj, T:\ListMor, i:\Int\\
  | ~& \forall j \in [ 1, \dots, \Length( L ) ]: \IsEqualForObjects\big(\Source( T[1] ), \Source( T[j] ) \big) \\
  \vdash &\PreCompose\big(\UniversalMorphismIntoDirectProduct( L, T ), \\
  &\ProjectionInFactorOfDirectProduct( L, i ) \big) =_{\Mor} T[i]
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &L:\ListObj, T:\ListMor, i:\Int\\
  |~ &()\\
  \vdash &\PreCompose\big(\InjectionOfCofactorOfCoproduct( L, i ),\\
  &\UniversalMorphismFromCoproduct( L, T ) \big) =_{\Mor} T[i]
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &A, B:\Obj, \tau_A, \tau_B:\Mor \\
  |~ &()\\
  \vdash &\PreCompose\big(\InjectionOfCofactorOfCoproduct( [A, B], 2 ),\\
  &\UniversalMorphismFromCoproduct( [A,B], [\tau_A, \tau_B] ) \big) =_{\Mor} \tau_B 
\end{align*}
\end{sequent}


\begin{sequent}
\begin{align*}
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\
  |~ &\IsEqualForMorphisms\big( \PreCompose( \tau_A, \alpha ), \PreCompose( \tau_B, \beta ) \big)\\
  \vdash &\PreCompose\big( \UniversalMorphismIntoFiberProduct( [\alpha, \beta], [\tau_A, \tau_B] ), \\
  &\ProjectionInFactorOfFiberProduct( [\alpha, \beta], 1 ) \big) =_{\Mor} \tau_A
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\
  |~ &\IsEqualForMorphisms\big( \PreCompose( \tau_A, \alpha ), \PreCompose( \tau_B, \beta ) \big)\\
  \vdash &\PreCompose\big( \UniversalMorphismIntoFiberProduct( [\alpha, \beta], [\tau_A, \tau_B] ), \\
  &\ProjectionInFactorOfFiberProduct( [\alpha, \beta], 2 ) \big) =_{\Mor} \tau_B
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\
  |~ &\IsEqualForMorphisms\big( \PreCompose( \alpha, \tau_A ), \PreCompose( \beta, \tau_B) \big)\\
  \vdash &\PreCompose\big( \InjectionOfCofactorOfPushout( [\alpha, \beta], 1 ), \\
  &\UniversalMorphismFromPushout( [\alpha, \beta], [\tau_A, \tau_B] )\big) =_{\Mor} \tau_A
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\
  |~ &\IsEqualForMorphisms\big( \PreCompose( \alpha, \tau_A ), \PreCompose( \beta, \tau_B) \big)\\
  \vdash &\PreCompose\big( \InjectionOfCofactorOfPushout( [\alpha, \beta], 2 ), \\
  &\UniversalMorphismFromPushout( [\alpha, \beta], [\tau_A, \tau_B] )\big) =_{\Mor} \tau_B
\end{align*}
\end{sequent}