категорная семантика логики

[jhanjaa]

Помогите, пожалуйста разобраться со следующим несоответствием:
При интерпретации теории доказательств в категории, морфизмы соответствуют классам эквивалентности доказательств. Первыми аксиомами являются $A \vdash A$ и, в моноидальных категориях, еще $\vdash I$, где $I$-тензорная единица, а вывод $\vdash I$ интерпретируется как морфизм $I \rightarrow I$. Оба вывода - и $A \vdash A$, и $\vdash I$, - единственные. В то же время, в категории множество морфизмов $A \rightarrow A$ может быть нетривиальным. Например, множество $C(I,I)$ стрелок $I \rightarrow I$ является моноидом. Эти стрелки разные, должны отвечать разным, неэквивалентным выводам, а в аксиомах предполагается, что вывод единственный. В чем дело?