generated at
逆射の一意性
from そこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』
逆射の一意性を示す

方針検討
恒等射を含む論理式は単位律しかない
多分これに代入すればなんかわかるだろう

証明
\forall A,B\in{\rm ob}(\mathscr A)\forall f:A\to B\forall g,g':B\to A.
\begin{dcases}g\circ f={\rm id}_A\land f\circ g={\rm id}_B\\g'\circ f={\rm id}_A\land f\circ g'={\rm id}_B\end{dcases}
\implies g\circ f={\rm id}_A\land f\circ g=f\circ g'
\because代入
\implies g\circ f={\rm id}_A\land g\circ f\circ g=g\circ f\circ g'
\implies {\rm id}_A\circ g={\rm id}_A\circ g'
\implies g=g'
\because単位律
\underline{\therefore\forall A,B\in{\rm ob}(\mathscr A)\forall f:A\to B\forall g,g':B\to A.\begin{dcases}g\circ f={\rm id}_A\land f\circ g={\rm id}_B\\g'\circ f={\rm id}_A\land f\circ g'={\rm id}_B\end{dcases}\implies g=g'\quad}_\blacksquare