3.1 Component equations for unit and counit

[aleksey-makarov]

I believe the domains for \varepsilon and R \varepsilon in the component wise equations are wrong, and the equations

\varepsilon_{L d} \circ L \etad = \id{L d} R \varepsilon{c} \circ \eta{R c} = \id_{R c}

should read as

\varepsilon_{L \circ R \circ L d} \circ L \etad = \id{L d} R \varepsilon{L \circ R c} \circ \eta{R c} = \id_{R c}

[BartoszMilewski]

It type checks: L \eta_d :: L d \to L R L d. \varepsilonc :: L R c \to c \varepsilon{L d} :: L R L d \to L d the composition goes from L d to L d.

[aleksey-makarov]

Is this correct:

\varepsilon_c :: L R c \to c

? I believe this should be

\varepsilon_{L R c} :: L R c \to c

Few lines above you had to introduce c' for the same reason

[BartoszMilewski]

I know it's a little confusing. In fact I get confused about it every time. Here's the trick: Draw three categories instead of two: C, D, and C again. The arrow starts at c, R takes it right, and L takes it right again to the second C. Id takes c directly from the leftmost C to the rightmost one. Then you drop epsilon_c between them.

[aleksey-makarov]

As far as I understand the lower index of a component of a natural transformation denotes domain (but not codomain) of that component. So component of natural transformation epsilon that goes from L R c to c is epsilon_{L R c} but not epsilon_c right?

[BartoszMilewski]

Think of a natural transformation between two functors F and G. Its component at c is a morphism alpha_c :: F c -> G c. Replace F with (L \circ R) and G with Id.

[aleksey-makarov]

Thank you very much.