Proof of trace respecting unit
Proposition (Trace respects unit)
(for
f
:
I
U A
and
g
:
X
U A
Y
in
C
):
=
Tr
X Y A
(
g
;
id
Y
f
)
=
(
id
X
f
);
g
Proof.
=
(Acyclic graph iso)
=
(Naturality of Tr)
=
(Yanking)
Back